|
|
|
Program
Monday, May 19th 2008
| Invited Speaker |
| 09:00 | Fabio Somenzi | A Pragmatic Approach to Synthesis |
| 10:00 | coffee break |
| | |
| Engines |
| 10:30 | Pavel Šimeček | I/O Efficient Model Checking (slides) |
| 11:00 | Robert Brummayer | Offline SMT for Arrays (slides) |
| 11:30 | Roberto Bruttomesso | Congruence Closure with Interpreted Selection and Concatenation (slides) |
| 12:00 | lunch |
| | |
| Foundations |
| 14:00 | Karin Greimel | Open Equivalence (slides) |
| 14:30 | Vasu Singh | Model Checking Transactional Memories (slides) |
| 15:00 | Marion Daubignard | Automated Proofs for Asymmetric Encryption (slides) |
| 15:30 | social event |
Tuesday, May 20th 2008
| Invited Speaker |
| 09:00 | Radek Pelanek | Experimental Work in Explicit Model Checking (slides) |
| 10:00 | coffee break |
| High-Level Verification |
| 11:00 | Nicola Bombieri | On the Abstraction of RTL Designs into TL Descriptions (slides) |
| 11:30 | Michael Tautschnig | FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement (slides) |
| 12:00 | Edvin Török | Static Memory Access Checking Using Symbolic Constraint Generation (slides) |
| 12:30 | lunch |
| | |
| Abstraction & Interpolation |
| 14:30 | Björn Wachter | Probabilistic CEGAR (slides) |
| 15:00 | Vijay D'Silva | Symbolic Extrapolation in Program Verification (slides, text) |
| 15:30 | Marco Murciano | Interpolant-Based Unbounded Model Checking |
| 16:00 | end |
Speakers
| Invited Speaker |
| Radek Pelanek |
Experimental Work in Explicit Model Checking (slides) |
| Abstract. We present BEEM (BEnchmarks for Explicit Model checkers) and experiments
performed over this benchmark set, e.g., study of properties of state
spaces, evaluation of error detection techniques, evaluation of techniques
for reducing memory consumption of model checkers. We will also discuss trends in experimental work and explicit model checking.
|
|
| Invited Speaker |
| Fabio Somenzi |
A Pragmatic Approach to Synthesis |
|
|
|
| Nicola Bombieri |
On the Abstraction of RTL Designs into TL Descriptions (slides) |
| Abstract. Transaction-level modeling (TLM) has been proposed as the leading
strategy to address the always increasing complexity of digital
systems. However, modeling a complex system completely at
transaction level (TL) could be inconvenient when IP cores are
available on the market, usually modeled at RT level. In this
context, modeling and verification methodologies based on
transactors allow one to reuse RTL IP-cores in TL-RTL mixed designs,
thus guaranteeing a considerable saving of time. Even if practical
advantages of such an approach are evident, mixed TL-RTL designs
cannot completely benefit from the well-known effectiveness provided
by TLM. Thus, this work proposes a methodology to abstract RTL IPs
into corresponding TL descriptions. The possibility of automating
the methodology and the issue concerning correctness of
the abstracted model are deeply analyzed.
|
|
| Robert Brummayer |
Offline SMT for Arrays (slides) |
| Abstract. Deciding satisfiability in the theory of arrays, particularly
in combination with bit-vectors, is essential for software and
hardware verification. We precisely describe how the lemmas
on demand approach can be applied to this decision problem.
In particular, we show how a propagation based algorithm can
be generalized to the extensional theory of arrays.
|
|
| Roberto Bruttomesso |
Congruence Closure with Interpreted Extraction and Concatenation (slides) |
| Abstract. This work describes a decision procedure for the theory of bit-vectors.
The procedure is based on a congruence closure algorithm, where
all operators are considered as uninterpreted, except for extraction and
concatenation, which are interpreted in their standard semantics.
We discuss the potentialities of the algorithm and we provide implementation
details.
|
|
| Marion
Daubignard | Automated Proofs for
Asymmetric Encryption (slides) | | Abstract. Chosen-ciphertext security is by now a
standard security property for asymmetric encryption. Many
generic constructions for building secure cryptosystems from
primitives with lower level of security have been proposed.
Providing security proofs has also become standard practice. There
is, however, a lack of automated verification procedures that
analyse such cryptosystems and provide security proofs. This paper
presents an automated procedure for analysing generic asymmetric
encryption schemes in the random oracle model. It has been applied
to several examples of encryption schemes. |
|
| Vijay D'Silva |
Symbolic Extrapolation in Program Verification (slides, text) |
|
| Karin Greimel |
Open Equivalence (slides) |
| Abstract. We argue that the usual trace-based notions of implication and
equivalence for linear temporal logics are too strong and should be
complemented by the weaker notions of open implication and open
equivalence. Although open implication is harder to compute, it can
be used to advantage both in model checking and in synthesis. We
describe an algorithm to compute open implication of Linear Temporal
Logic formulas with an asymptotically optimal complexity. We also
show how to compute open implication while avoiding Safra~Rs
construction and study the difference between trace-based
equivalence and open equivalence. We have implemented an
open-implication solver for Generalized Reactivity( 1)
specifications. In a case study, we show that open equivalence can
be used to justify the use of an alternative specification that
allows us to synthesize much smaller systems in far less time.
|
|
| Marco Murciano |
Interpolant-Based Unbounded Model Checking |
| Abstract. Craig interpolants have recently attained very good results in Unbounded Model Checking, by combining automated abstraction and implicit variable quantification.
Interpolants are generated starting from refutation proofs, that modern SAT solvers produce as a byproduct of unsatisfiable runs.
The talk will focus on advantages and limitations of interpolants, and it will introduce some recent advancements in SAT-based Unbounded Model Checking, where the general idea of interpolation is extended, by considering abstract (over-approximate) behaviors not generated from refutation proofs.
Localization abstraction, implications and equivalences, as well as ternary abstraction, will be described within an interpolation-based verification framework.
Preliminary experimental results, showing the overall benefits of the proposed techniques, will be finally presented.
|
|
| Pavel Šimeček |
I/O Efficient Model Checking (slides) |
| Abstract. One way to increase a memory available to model checking algorithms is
to employ the external memory, namely hard disks. Unfortunately, no
DFS-based algorithm behaving efficiently in external memory
environment is known. We show how to adapt an existing BFS-based
accepting cycle detection algorithms OWCTY and MAP to the I/O
efficient setting and compare their I/O efficiency and practical
performance to the existing I/O efficient LTL model checking approach
of Edelkamp and Jabbar. New algorithms exhibit similar I/O complexity
with respect to the size of the graph while they avoid quadratic
increase in the size of the graph. Therefore, the number of I/O
operations performed is significantly lower and the algorithm exhibits
better practical performance.
|
|
| Vasu Singh |
Model Checking Transactional Memories (slides) |
| Abstract. With the inherent problems in writing correct and efficient concurrent code, a recent concurrent programming paradigm called 'transactional memory' has gained popularity. Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memory. We reduce this verification problem to a finite state problem in two steps. First, we show that every STM that enjoys certain structural properties either violates a safety or liveness requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. Second, we use a model checker to prove the requirement for the STM applied to a most general program with two threads and two variables. In the safety case, the model checker constructs a simulation relation between two carefully constructed finite-state transition systems, one representing the given STM applied to a most general program, and the other representing a most liberal safe STM applied to the same program. In the liveness case, the model checker analyzes fairness conditions on the given STM transition system. We illustrate the use of the method by proving the correctness of several STMs, including two-phase locking, DSTM, TL2, and optimistic concurrency control.
|
|
| Michael Tautschnig |
FShell: Systematic Test Case Generation for
Dynamic Analysis and Measurement (slides) |
| Abstract. Although the principal analogy between counterexample generation and
white box testing has been repeatedly addressed, the usage patterns
and performance requirements for software testing are quite
different from formal verification. Our tool FShell provides a
versatile testing environment for C programs which supports both
interactive explorative use and a rich scripting language. More than
a frontend for software model checkers, FShell is designed as a
database engine which dispatches queries about the program to
program analysis tools. We report on the integration of CBMC into
FShell and describe architectural modifications which support
efficient test case generation.
|
|
| Edvin Török |
Static Memory Access Checking Using Symbolic Constraint Generation (slides) |
| Abstract. Memory errors such as bounds violations, use after free, etc. are often
hard to find and can be the source of security vulnerabilities.
Tracking them down or proving their absence requires an automated tool.
The talk presents such a static analysis tool based on generating
constraints which must hold for each memory access. The tool is built
using the LLVM Compiler Infrastructure and passes the constraints to an
SMT-Solver, which gives a verdict on the safety of a memory access.
Using the LLVM intermediate representation has the advantage of taking
into consideration the implementation of modular arithmetic, and the
arising issues of integer arithmetic overflow. Furthermore, the generated
constraints are easily transformable into logic formulas for the
solver. These are generated in the smt-lib benchmark standard format,
facilitating a choice of solvers.
We also address situations that do not generate runtime errors, but are
logical errors, such as overflowing the boundaries of structure fields.
In order for such a tool to be useful, it needs to have a low false
positive rate. Several measures are taken to reach this goal: constraints
are generated symbolically (dealing only with constants is of limited
use); a path-sensitive flow analysis is performed and warnings are only
issued if the unsafe instruction is ever reached. Reporting of potential
integer overflows is filtered and only done if they affect the safety of
a memory access.
To help the user understand easily what and where the problem is, we also
give an example of values that lead to the unsafe memory access. Thus the
user can easily follow the control flow, without having to follow the
reasoning behind complex logic formulas. The constraint violations that
don't always happen are registered as a function's summary, and used to
build an interprocedural analysis.
|
|
| Björn Wachter |
Probabilistic CEGAR (slides) |
| Abstract. Probabilistic models are widely used to analyze embedded, networked, and more recently biological systems. The goal of this research is to develop analysis techniques for large or even infinite probabilistic models. To this end, concise abstractions are crucial, abstractions that are precise enough to obtain the desired information and yet small enough to be effeciently analyzable. We develop abstraction refinement techniques for probabilistic systems to find concise abstractions. I will present an abstraction refinement scheme based on counterexample analysis. Different than in the non-probabilistic setting, we consider counterexamples that are Markov chains and not paths. Cycles and probabilistic branching in these Markov chains make the task of counterexample analysis more
|
|
|
