14th International Symposium on Automated Technology for Verification and Analysis
October 17 - 20, 2016, Chiba, Japan
In logic synthesis, the search space is infinite in the sense that any number of gates can be connected using any topology to come up with the best circuit under performance and other constraints. In formal verification, to achieve full coverage, an n-input circuit must be checked either explicitly or implicitly using the complete set of 2n input values. There are, however, situations when the possible circuit topologies are limited. Logic optimization methods, in general, do not change circuit topologies dramatically. Most of them are based on series of local circuit transformations. In this paper, we discuss formal verification of circuits produced by logic synthesis where the search space is limited, and only gates or subcircuits are transformed whereas their interconnections never change. If there are p possible transformations for each gate or subcircuit, and there are m gates or subcircuits in the entire circuit, the number of all possible transformations for the entire circuit is pm. Logic synthesis with this restriction attempts to find the best circuit among the pm alternatives. The logic synthesis problem can be formulated as a sequence of incremental SAT problems and the complete set of test patterns can be computed, which detects all possible errors in the synthesized circuit. As long as the search space is limited to the pm alternatives, such complete set of test patterns can be used for formal verification. The number of test patterns needed in this case is experimentally shown to be very small, e.g., a few hundred, even for circuits having several hundred inputs and several thousand gates. With the complete set of test patterns generated for the circuit transformations, logic synthesis and formal verification are unified in the sense that the small number of test patterns allows for logic synthesis with 100% correctness.
A crucial problem in software security is the detection of side-channels. Information gained by observing non-functional properties of program executions (such as execution time or memory usage) can enable attackers to infer secret information (such as a password). In this talk, I will discuss how symbolic execution, combined with a model counting constraint solver, can be used for quantifying side-channel leakage in Java programs. In addition to computing information leakage for a single run of a program, I will also discuss computation of information leakage for multiple runs for a type of side channels called segmented oracles. In segmented oracles, the attacker is able to explore each segment of a secret (for example each character of a password) independently. For segmented oracles, it is possible to compute information leakage for multiple runs using only the path constraints generated from a single run symbolic execution. These results have been implemented as an extension to the symbolic execution tool Symbolic Path Finder (SPF) using the SMT solver Z3 and two model counting constraint solvers LattE and ABC.
Limit-deterministic Büchi automata can replace deterministic Rabin automata in
probabilistic model checking algorithms, and can be significantly smaller. We
present a direct construction from an LTL formula to a limit-deterministic Büchi
automaton. Our translation is compositional and has a clear logical structure.
Moreover, due to its special structure, the resulting automaton can be used not
only for qualitative, but also for quantitative verification of Markov Decision
Processes, using the same model checking algorithm as for deterministic
automata. This allows one to reuse existing efficient implementations of this
algorithm without any modification. Our construction yields much smaller
automata for formulas with deep nesting of modal operators and performs at least
as well as the existing approaches on general formulas.
Joint work with Stefan Jaax, Jan Kretinsky, and Salomon Sickert
Here we first introduce Quantified Boolean Formula(QBF) based approaches to logic synthesis and testing in general including automatic corrections of designs. It is formulated as: If some appropriate values are assigned to what we call programmable variables, the resulting circuits behaves as our intentions for all possible input values, that is, they become the ones whose logic functions are the intended ones. In this paper we only target combinational circuits and sequential circuits which are time-frame expanded by fixed times. The QBF problems are solved by repeatedly applying SAT solvers, not QBF solvers, with incremental additions of new constraints for each iteration which come from counter examples for the SAT problems. The required numbers of iterations until solutions are obtained are experimentally shown to be pretty small (in the order of tens) even if there are hundreds of inputs, regardless of the fact that they have exponentially many value combinations. Then the applications of the proposed methodology to logic synthesis, logic debugging, and automatic test pattern generations (ATPG) for multiple faults are discussed with experimental results. In the case of ATPG, a test pattern is generated for each iteration, and programmable variables can represent complete sets of functional and multiple faults, which are the most general faults models.
The goal of string analysis techniques is to determine the set of values that string expressions can take during program execution. Like many other program analysis problems, it is not possible to precisely determine the set of string values that can reach a program point. However, one can compute over or under-approximations of possible string values. If the approximations are precise enough, they can enable analyzers to demonstrate existence or non-existence of bugs in string manipulating code. Analyzing string manipulating code is of interest to many areas of current research in program analysis and verification since string manipulation is a crucial part of modern software systems. For example string manipulation is extensively used in input validation and sanitization and in dynamic code and query generation. String analysis has been an active research area in the last decade, resulting in a wide variety of string analysis techniques. In this tutorial, we will discuss automated string analysis techniques, focusing particularly on automata-based static string analysis. Topics we plan to discuss include symbolic string analysis, string constraint solving, symbolic execution using string constraints, automated repair for string manipulating code, and model counting for string constraints.
A parametrized system is a parallel composition of some N>2 similar processes. Uniform verification attempts to verify such a composition for every value of N. This tutorial will describe some of the main methodologies for achieving such a task: finite abstractions, regular model checking, and generalizations from few processes to the many.
Population protocols (Angluin et al., PODC 2004) are a formal model of sensor
networks consisting of identical mobile devices. When two devices come into the
range of each other, they interact and change their states. Computations are
infinite sequences of pairwise interactions where the interacting processes are
picked by a fair scheduler.
A population protocol is well specified if for every initial configuration C of devices
and for every fair computation starting at C, all devices eventually agree on a
consensus value that only depends on C. If a protocol is well-specified, then it is
said to compute the predicate that assigns to each initial configuration its
consensus value. The main two verification problems for population protocols are:
Is a given protocol well-specified? Does a given protocol compute a given
While the class of predicates computable by population protocols was already
established in 2007 (Angluin et al., Distributed Computing), the decidability of the
verification problems remained open until 2015, when my colleagues and I finally
proved it (Esparza et al., CONCUR 2015, improved version to appear in Acta
Informatica). In the talk I report on our results and discuss some new
Joint work with Pierre Ganty, Jerome Leroux, and Rupak Majumdar
J. Brunel, D. Kuperberg and D. Chemouil. On Finite Domains in First-Order Linear Temporal Logic
R. Brenguier and V. Forejt. Decidability Results for Multi-objective Stochastic Games
A. Reynolds, R. Iosif, C. Serban and T. King. A Decision Procedure for Separation Logic in SMT
Philipp J. Meyer and M. Luttenberger. Solving Mean-Payoff Games on the GPU (tool paper)
Ó. Martín, A. Verdejo and N. Martí-Oliet. Synchronous products of rewrite systems
B. Finkbeiner, H. Seidl and C. Müller. Specifying and V. Secrecy in Workflows with Arbitrarily Many Agents
T. Nguyen Lam, B. Fischer, S. L. Torre and G. Parlato. Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs
N. Benes, L. Brim, M. Demko, S. Pastva and D. Safránek. Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems
R. Iosif and A. Sangnier. How hard is it to verify flat affine counter systems with the finite monoid property?
F. Avellaneda, S. D. Zilio and J. Raclet. Solving Language Equations using Flanked Automata
A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renault and L. Xu. Spot 2.0 - a framework for LTL and omega-automata manipulation (tool paper)
S. Sickert and J. Kretinsky. MoChiBA: Probabilistic LTL Model Checking using limit-deterministic Büchi Automata (tool paper)
A. Abate, M. Ceska and M. Kwiatkowska. Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations
T. Brazdil, A. Kucera and P. Novotný. Optimizing the Expected Mean Payoff in Energy Markov Decision Processes
T. Quatmann, C. Dehnert, N. Jansen, S. Junges and J. Katoen. Parameter Synthesis for Markov Models: Faster Than Ever
N. Jansen, C. Dehnert, B. L. Kaminski, J. Katoen and L. Westhofen. Bounded Model Checking for Probabilistic Programs
C. Baier, H. de Meer, S. Klüppelholz, F. Niedermeier and S. Wunderlich. Greener Bits: Formal Analysis of Demand Response
A. Duret-Lutz, F. Kordon, D. Poitrenaud and E. Renault. Heuristics for Checking Liveness Properties with Partial Order Reductions
T. Neele, A. Wijs, D. Bosnacki and J. v. d. Pol. Partial-Order Reduction for GPU Model Checking
P. Metzler, H. Saissi, P. Bokor, R. Hesse and N. Suri. Efficient Verification of Program Fragments: Eager POR
B. Finkbeiner and H. Torfah. Synthesizing Skeletons for Reactive Systems
S. Ben-David, M. Chechik and S. Uchitel. Observational Refinement and Merge for Disjunctive MTSs
X. Li and N. Kobayashi. Equivalence-Based Abstraction Refinement for muHORS Model Checking
K. Wimmer, R. Wimmer, C. Scholl and B. Becker. Skolem Functions for DQBF
H. Roehm, J. Oehlerking, T. Heinz and M. Althoff. STL Model Checking of Continuous and Hybrid Systems
M. Marescotti, A. Hyvärinen and N. Sharygina. Clause Sharing and Partitioning for Cloud-Based SMT Solving
D. Deininger, R. Dimitrova and R. Majumdar. Symbolic Model Checking for Factored Probabilistic Models
J. Hua and S. Khurshid. A Sketching-Based Approach for Debugging Using Test Cases
S. D. Oliveira, S. Bensalem and V. Prevosto. Polynomial invariants by linear algebra
R. Qiu, C. Pasareanu and S. Khurshid. Certified Symbolic Execution
P. Cadek, J. Strejcek and M. Trtík. Tighter Loop Bound Analysis