FLOC 2022: FEDERATED LOGIC CONFERENCE 2022
PERR ON THURSDAY, AUGUST 11TH

View: session overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments
09:30-10:30 Session 124B: Keynote Talk

Title: Regression verification of unbalanced recursive functions with multiple calls

Speaker:  Chaked R.J.Sayedoff  and Ofer Strichman ,  Technion, Israel

Abstract: Given two programs p1 and p2, typically two versions of the sameprogram, the goal of \emph{regression verification} is to mark pairs offunctions from p1 and p2 that are equivalent, given a definitionof equivalence. The most common definition is that of \emph{partialequivalence}, namely that the two functions emit the same output if theyare fed with the same input and they both terminate. The strategy usedby the Regression Verification Tool (RVT) is to progress bottom up onthe call graphs of P1,P2, abstract those functions that were alreadyproven to be equivalent with uninterpreted functions, turn loops intorecursion, and abstract the recursive calls also with uninterpretedfunctions. This enables it to create verification conditions in the formof small programs that are loop- and recursion-free. This method workswell for recursive functions as long as they are in sync, and typicallyfails otherwise. In this work we study the problem of provingequivalence when the two recursive functions are not in sync.Effectively we extend  previous work that studied this problem forfunctions with a single recursive call site, to the general case. Wealso introduce a method for detecting automatically the unrolling thatis necessary for making two recursive functions synchronize, whenpossible. We show examples of pairs of functions with multiple recursivecalls that can now be proven equivalent with our method, but cannot beproven equivalent with any other automated verification system.

Location: Ullmann 305
09:30
Regression verification of unbalanced recursive functions with multiple calls

ABSTRACT. Given two programs $p_1$ and $p_2$, typically two versions of the same program, the goal of \emph{regression verification} is to mark pairs of functions from $p_1$ and $p_2$ that are equivalent, given a definition of equivalence. The most common definition is that of \emph{partial equivalence}, namely that the two functions emit the same output if they are fed with the same input and they both terminate. The strategy used by the Regression Verification Tool (RVT) is to progress bottom up on the call graphs of $P_1,P_2$, abstract those functions that were already proven to be equivalent with uninterpreted functions, turn loops into recursion, and abstract the recursive calls also with uninterpreted functions. This enables it to create verification conditions in the form of small programs that are loop- and recursion-free. This method works well for recursive functions as long as they are in sync, and typically fails otherwise. In this work we study the problem of proving equivalence when the two recursive functions are not in sync. Effectively we extend previous work that studied this problem for functions with a single recursive call site, to the general case. We also introduce a method for detecting automatically the unrolling that is necessary for making two recursive functions synchronize, when possible. We show examples of pairs of functions with multiple recursive calls that can now be proven equivalent with our method, but cannot be proven equivalent with any other automated verification system.

10:30-11:00Coffee Break
11:00-12:30 Session 125L: Research Papers
Location: Ullmann 305
11:00
Compositional Approaches to Games in Model Checking

ABSTRACT. Games are an important tool in formal verification techniques such as model checking. Therefore, efficient solutions for games are essential in formal verification. Compositionality is a property that reasoning about a big system can be reduced to reasoning about its constituent parts, and thus it often enables efficient divide-and-conquer-type algorithms.

We present a compositional solution of parity games. This is achieved by adding open ends to the usual notion of parity games. Our compositional solution is based on compact closed categories and compact closed functors between them.

We also present a compositional solution of mean payoff games. We have conducted experiments targeting mean payoff games. The experiment results show that the compositionality property of our approach is advantageous, especially when a target mean payoff game is a large one that is built from well-separated components mean payofff games.

11:30
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques (Extended Abstract)
PRESENTER: Yu-Yang Lin

ABSTRACT. We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, novel up-to techniques, and lightweight state invariant annotations. This yields an equivalence verification technique with no false positives or negatives. The technique is bounded-complete, in that all inequivalences are automatically detected given large enough bounds. Moreover, several hard equivalences are proved automatically or after being annotated with state invariants. We realise the technique in a tool prototype called Hobbit and benchmark it with an extensive set of new and existing examples. Hobbit can prove many classical equivalences including all Meyer and Sieber examples.

12:00
Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems
PRESENTER: Kasper Hagens

ABSTRACT. One approach to proving equivalence of two functions in imperative programming languages is by an automatic conversion of the functions to an equivalent Logically Constrained Term Rewriting Systems, for which equivalence can be proved using rewriting induction, either fully automatically or guided by the user. We will relate ongoing work to build on this approach, by exploring three new lemma generation techniques.

!!!ATTENTION: THIS IS A CROSS SUBMISSION OF A PAPER WITH THE SAME TITLE HANDED IN FOR WPTE.!!!

12:30-14:00Lunch Break

Lunches will be held in Taub hall and in The Grand Water Research Institute.

14:00-15:00 Session 127L: Research Papers
Location: Ullmann 305
14:00
Implementing a Path Based Equivalence Checker for Petri net based Models of Programs

ABSTRACT. User written programs, when transformed by optimizing and parallelizing compilers, can be incorrect, if the compiler is not trusted. So, establishing the validity of these trans- formations is a crucial and challenging task. For program verification, the PRES+ (Petri net Representation of Em- bedded Systems) is now well accepted as a model to capture the data and control flow of a program. In this paper, an effi- cient path based equivalence checking method using a simple PRES+ model (which is easier to generate from a program) for validating several optimizing and parallelizing transfor- mations is proposed. The experimental results demonstrate the efficiency of the method

14:30
Generating Mutation Tests Using an Equivalence Prover

ABSTRACT. Creating test cases and assessing their quality is a necessary but time-consuming part of software development. Mutation Testing facilitates this process by introducing small syntactic changes into the program and thereby creating mutants. The quality of test cases is then measured by their ability to differentiate between those mutants and the original program. Previous studies have also explored techniques to automatically generate test inputs from program mutants. However, the symbolic approaches to this problem do not handle unbounded loops within the program. In this paper, we present a method using the equivalence prover LLRêve to generate test cases from program mutants. We implemented the method as a pipeline and evaluated it on example programs from the learning platform c4learn as well as programs from the library diet libc. Our results have shown that this method takes up to multiple hours to run on these programs, but the generated test cases are able to detect half of the known errors. As an extension to the method, we also present mutations which introduce an additional parameter into the program. We then show on an example that a finite set of test cases can be sufficient to kill the mutant for all values of the parameter.

15:30-16:00Coffee Break
16:00-17:00 Session 131J: Invited Talk

Title: Compositional relational reasoning via operational game semantics

Andrzej Murawski (University of Oxford)

Abstract: We use operational game models as a guide to develop relational techniques for establishing contextual equivalences with respect to contexts drawn from a hierarchy of four call-by-value higher-order languages,with either general or ground-type references and with either call/cc or no control operator. In game semantics, the differences between the contexts can be captured by the absence or presence of the O-visibility and O-bracketing conditions.

The proposed technique, which we call Kripke Normal-Form Bisimulations, combines insights from normal-form bisimulation and Kripke-style logical relations with game semantics. In particular, the role of the heap is abstracted away using Kripke-style world transition systems. The differences between the four kinds of contexts manifest themselves through simple local conditions that can be shown to correspond to O-visibility and O-bracketing, where applicable.

The technique is sound and complete by virtue of correspondence with operational game semantics. Moreover, the framework developed in the paper sheds a new light on other related developments, such as backtracking and private transitions in Kripke logical relations, which can be related to specific phenomena in game models.

 

This is joint work with Guilhem Jaber (Universite de Nantes).

 

Location: Ullmann 305
16:00
Compositional relational reasoning via operational game semantics

ABSTRACT. We use operational game models as a guide to develop relational techniques for establishing contextual equivalences with respect to contexts drawn from a hierarchy of four call-by-value higher-order languages, with either general or ground-type references and with either call/cc or no control operator. In game semantics, the differences between the contexts can be captured by the absence or presence of the O-visibility and O-bracketing conditions.

The proposed technique, which we call Kripke Normal-Form Bisimulations, combines insights from normal-form bisimulation and Kripke-style logical relations with game semantics. In particular, the role of the heap is abstracted away using Kripke-style world transition systems. The differences between the four kinds of contexts manifest themselves through simple local conditions that can be shown to correspond to O-visibility and O-bracketing, where applicable.

The technique is sound and complete by virtue of correspondence with operational game semantics. Moreover, the framework developed in the paper sheds a new light on other related developments, such as backtracking and private transitions in Kripke logical relations, which can be related to specific phenomena in game models.

This is joint work with Guilhem Jaber (Universite de Nantes).

18:00-19:30Workshop Dinner (at the Technion, Taub Terrace Floor 2) - Paid event