ABSTRACT. This talk is a tutorial on interpolation in verification.

Model checking is an automatic approach to formally verify that a given system satisfies a given specification. SAT-based model checking is most efficient in finding bugs in large systems. When combined with interpolation, it can also provide full verification. We describe the use of interpolation in SAT-based model checking and survey several approaches to enhance its power. We will assume no previous knowledge on model checking or interpolation. All the needed background will be given.

ABSTRACT. We present a new application of interpolants in the context of two-player games. Two-player games is a useful formalism for the synthesis of reactive systems, with applications in device driver development, hardware design, industrial automation, etc.In particular, we consider reachability games over a finite state space, where the first player (the controller) must force the game into a given goal region given any valid behaviour of the second player (the environment). In this work, we focus on the strategy extraction problem in the context of a new counter example guided SAT-based algorithm for solving reachability games, recently proposed by Narodytska et al. We demonstrate how interpolants can be used to find a winning strategy.

ABSTRACT. An integral part of all debugging activities is the task of fault localization. Most existing fault localization techniques rely on the availability of high quality test suites because they work by comparing failing and passing runs to identify the cause of an error. This limits their applicability. One alternative are techniques that statically analyze an error trace of the program without relying on additional passing runs to compare against. Particularly promising are novel proof-based approaches that leverage the advances in automated theorem proving. These approaches encode error paths into \emph{error trace formulas}. An error trace formula is an unsatisfiable logical formula. A refutation proof of this formula captures the reason why the execution of the error trace fails. By applying an automated theorem prover to obtain such proofs, the relevant portions of the trace can be automatically identified without relying on the availability of test suites. For example, in our previous work, we have used Craig interpolation to extract formulas from the obtained refutation proof. These so-called \emph{error invariants} provide an explanation of the error for a given position in the trace and can be used for more effective static slicing.

In particular, we encode the error trace into a logical formula whose satisfying assignment exactly corresponds to the states that are observed during the concrete execution of the trace. The encoding uses standard symbolic execution techniques. Namely, we first convert the trace into static single-assignment form, then translate each individual statement into a logical constraint, and finally conjoin all the constraints to a single formula. We call the resulting conjunction the \emph{error trace formula} of the trace. By conjoining the error trace formula with the property that is violated at the end of the trace, we obtain an unsatisfiable formula. Since this property is violated at the end of the execution of the error trace, this formula is contradictory (i.e. UNSAT). We then use an interpolating SMT solver to generate an error invariant for each position in the trace from a refutation proof of the unsatisfiable formula. The computed error invariants have two important properties: (1) they are satisfied by the concrete state that is observed at the respective position in the trace; and (2) any execution of the remainder of the trace starting from that position with a state that satisfies the error invariant will still violate the property at the end of the trace.

The generated error invariants are then propagated along the trace to identify maximal subtraces such that the same error invariant holds at both the beginning and the end of the subtrace. From the two properties of error invariants, it follows that the statements between these two positions are irrelevant for understanding the bug and, hence, can be sliced from the trace. We proceed like this for the entire error trace to produce the abstract slice.

While proof-based fault localization techniques are a promising alternative to dynamic techniques, they have practical limitations that have not been addressed in previous work. Precisely capturing the behavior of an erroneous program requires modeling such features as dynamic memory allocation, function calls, inputs, and loops, over traces that can extend to large numbers of instructions. Although mathematical techniques exist to handle these complexities, their implementation in current off-the-shelf theorem provers is often far from robust. For example, heap accesses are traditionally handled using array theories. Unfortunately, most provers lack interpolation procedures for the theory of arrays, making it difficult to automatically infer invariants about heap allocated objects.

To address these shortcomings of purely static approaches, we propose a novel fault localization technique that combines dynamic and static analysis of the error trace. In particular, we note that given an executable error trace, we can determine the concrete value of every variable, and every memory address, using a standard debugger. This information can then be used to dramatically simplify the encoding of the error trace for static analysis. Instead of relying on complex mathematical theories to reason about pointer aliasing, we can directly determine which memory location a pointer references using the debugger. If a trace contains too many statements to analyze using a theorem prover, we can split the trace into subtraces, and use the program states observed during the concrete execution to seed the analysis of the individual subtraces.

We have conducted a case study where we applied our new algorithm to error traces generated from faulty versions of UNIX utils such as gzip and sed. Our case study indicates that our concolic fault localization scales to real-world error traces and generates useful error diagnoses.

ABSTRACT. Feasible interpolation has been proved for several proof systems based on integer linear programming. To prove such a theorem one has to design a polynomial time algorithm. The methods which are used to design these algorithms range from a very simple algorithm, used in the cutting plane proof system, to semidefinite programming, used in a version of Lovasz-Schrijver proof system. This reflects the increasing strength of the proof systems.

ABSTRACT. The third round of the Kurt Gödel Research Prize Fellowships Program, under the title: Connecting Foundations and Technology, aims at supporting young scholars in early stages of their academic careers by offering highest fellowships in history of logic, kindly supported by the John Templeton Foundation. Young scholars being less or exactly 40 years old at the time of the commencement of the Vienna Summer of Logic (July 9, 2014) will be awarded one fellowship award in the amount of EUR 100,000, in each of the following categories:

• Logical Foundations of Mathematics,
• Logical Foundations of Computer Science, and
• Logical Foundations of Artificial Intelligence

The following three Boards of Jurors were in charge of choosing the winners:

• Logical Foundations of Mathematics: Jan Krajíček, Angus Macintyre, and Dana Scott (Chair).
• Logical Foundations of Computer Science: Franz Baader, Johann Makowsky, and Wolfgang Thomas (Chair).
• Logical Foundations of Artificial Intelligence: Luigia Carlucci Aiello, Georg Gottlob (Chair), and Bernhard Nebel.

http://fellowship.logic.at/

ABSTRACT. The aim of the FLoC Olympic Games is to start a tradition in the spirit of the ancient Olympic Games, a Panhellenic sport festival held every four years in the sanctuary of Olympia in Greece, this time in the scientific community of computational logic. Every four years, as part of the Federated Logic Conference, the Games will gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At the Award Ceremonies, the competition organizers will have the opportunity to present their competitions to the public and give away special prizes, the prestigious Kurt Gödel medals, to their successful competitors. This reinforces the main goal of the FLoC Olympic Games, that is, to facilitate the visibility of the competitions associated with the conferences and workshops of the Federated Logic Conference during the Vienna Summer of Logic.

This award ceremony will host the

• 3rd Confluence Competition (CoCo 2014);
• Configurable SAT Solver Challenge (CSSC 2014);
• Ninth Max-SAT Evaluation (Max-SAT 2014);
• QBF Gallery 2014; and
• SAT Competition 2014 (SAT-COMP 2014).

ABSTRACT. (see attached abstract)

ABSTRACT. It is useful to consider projection and forgetting as second-order operators with elimination as associated computational processing: They can be nested and further second-order operators can be defined in terms of them. In the presentation, it is outlined for a variety of properties, concepts and tasks in knowledge representation and reasoning how these can be expressed in this framework.

ABSTRACT. Craig interpolation is used in solving bounded model checking (BMC) SAT and SMT problems.

In 2012, Teige et al. succeeded to compute interpolants for stochastic boolean satisfiability problems, i.e. SSAT.

That was achieved by defining sound and complete resolution calculus for SSAT and computing the Craig interpolation for (A and B and not S_{A,B}), where not S_{A,B} represents a conflict clause of A and B. Consequently, one can obtain two interpolants for the formula \Phi: A and B, where one interpolates A, and the second one interpolates B.

As a result of that, an approach to solve efficiently stochastic bounded model checker problems, e.g. MDPs, was addressed by using SSAT interpolation.

In this work we present a notion of Craig Interpolation for the stochastic modulo theories framework i.e. SSMT. An SSMT formula consists of free and quantified variables where the latter variables are bound to discrete domains by existential or randomized quantifiers. In the case of a randomized variable, the variable can be assigned to one of its domain values with a certain probability, where the summation of all probabilities of the same variable has to be one. The significance of SSMT comes from the fact that one can encode probabilistic hybrid automata problems as SSMT formulae.

Our approach to compute the Craig interpolation for SSMT is as follows: we assume that arithmetic constraints can be relaxed as simple bounds by using interval constraint propagation (ICP) as implemented in iSAT tool. After that, we define a sound and relatively-complete resolution calculus for SSMT formula as done in case of SSAT, such that if a conflict clause is derived with a certain probability, then the latter probability is a safe upper bound of the real satisfaction probability of the SSMT formula. Then we extend P'udlak rules in a way such that simple bounds are treated as literals and if a conflict clause is derived, then we get a generalized Craig interpolation for the whole formula (A and B and not S_{A,B}).

Finally, we adapt BMC to the probabilistic case, i.e. PBMC by encoding a step-bounded reachability problems as an SSMT formula, where a generalized Craig interpolation is used to compute an upper bound of the maximum probability of reaching the target states.