synthesis

Proving Functional Program Equivalence via Directed Lemma Synthesis
Proving equivalence between functional programs is a fundamental problem in program verification, which often amounts to reasoning …
PDF Cite
Proving Functional Program Equivalence via Directed Lemma Synthesis
Indecision and Delays are the Parents of Failure
The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and …
PDF Cite Code Slides Video DOI
Indecision and Delays are the Parents of Failure
Verification and Synthesis of Time-Delayed Dynamical Systems
Conventional embedded systems have over the past two decades vividly evolved into an open, interconnected form that integrates …
Cite Slides CAS-President Special Award
Verification and Synthesis of Time-Delayed Dynamical Systems
What's to Come is Still Unsure
The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and …
PDF Cite Code Slides Video DOI Distinguished Paper Award
What's to Come is Still Unsure
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
An algorithm for generating interpolants for formulas which are conjunctions of quadratic polynomial inequalities (both strict and …
PDF Cite Code Slides DOI
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF