Counterexample-guided inductive synthesis for probabilistic systems

Author(s):  
Milan Češka ◽  
Christian Hensel ◽  
Sebastian Junges ◽  
Joost-Pieter Katoen
Author(s):  
Satoshi Kura ◽  
Hiroshi Unno ◽  
Ichiro Hasuo

AbstractWe present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workflow of CounterExample Guided Inductive Synthesis (CEGIS). CEGIS is an iterative learning model where, at each iteration, (1) a synthesizer synthesizes a candidate solution from the current examples, and (2) a validator accepts the candidate solution if it is correct, or rejects it providing counterexamples as part of the next examples. Our main novelty is in the design of a synthesizer: building on top of a usual decision tree learning algorithm, our algorithm detects cycles in a set of example transitions and uses them for refining decision trees. We have implemented the proposed method and obtained promising experimental results on existing benchmark sets of (non-)termination verification problems that require synthesis of piecewise-defined lexicographic affine ranking functions.


2020 ◽  
Vol 64 (7) ◽  
pp. 1523-1552
Author(s):  
Daniel Neider ◽  
P. Madhusudan ◽  
Shambwaditya Saha ◽  
Pranav Garg ◽  
Daejun Park

Abstract We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counterexample guided inductive synthesis principle and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic. Our experiments show that our invariant synthesis framework based on non-provability information can both effectively synthesize inductive invariants and adequately strengthen contracts across a large suite of programs. This work is an extended version of a conference paper titled “Invariant Synthesis for Incomplete Verification Engines”.


IEEE Access ◽  
2020 ◽  
Vol 8 ◽  
pp. 207485-207498
Author(s):  
Konstantin Chukharev ◽  
Dmitrii Suvorov ◽  
Daniil Chivilikhin ◽  
Valeriy Vyatkin

10.29007/msr8 ◽  
2018 ◽  
Author(s):  
Heinz Riener ◽  
Robert Koenighofer ◽  
Goerschwin Fey ◽  
Roderick Bloem

We present a simple, yet flexible parameter synthesis and repair approach for Cyber-Physical Systems (CPS). The user defines the behavior of a CPS, a set of (un)safe states, and a generic template for an inductive invariant using Satisfiability Modulo Theories (SMT) formulas. Counterexample-Guided Inductive Synthesis (CEGIS) is then used to compute values for open parameters and a concrete invariant to prove that all unsafe states are unreachable. Using templates for expressions, the approach can also be used for CPS repair. We present a proof-of-concept tool, optimizations, and first experiments.


2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-26
Author(s):  
Guoqiang Zhang ◽  
Yuanchao Xu ◽  
Xipeng Shen ◽  
Işıl Dillig

Many data processing systems allow SQL queries that call user-defined functions (UDFs) written in conventional programming languages. While such SQL extensions provide convenience and flexibility to users, queries involving UDFs are not as efficient as their pure SQL counterparts that invoke SQL’s highly-optimized built-in functions. Motivated by this problem, we propose a new technique for translating SQL queries with UDFs to pure SQL expressions. Unlike prior work in this space, our method is not based on syntactic rewrite rules and can handle a much more general class of UDFs. At a high-level, our method is based on counterexample-guided inductive synthesis (CEGIS) but employs a novel compositional strategy that decomposes the synthesis task into simpler sub-problems. However, because there is no universal decomposition strategy that works for all UDFs, we propose a novel lazy inductive synthesis approach that generates a sequence of decompositions that correspond to increasingly harder inductive synthesis problems. Because most realistic UDF-to-SQL translation tasks are amenable to a fine-grained decomposition strategy, our lazy inductive synthesis method scales significantly better than traditional CEGIS. We have implemented our proposed technique in a tool called CLIS for optimizing Spark SQL programs containing Scala UDFs. To evaluate CLIS, we manually study 100 randomly selected UDFs and find that 63 of them can be expressed in pure SQL. Our evaluation on these 63 UDFs shows that CLIS can automatically synthesize equivalent SQL expressions in 92% of the cases and that it can solve 2.4× more benchmarks compared to a baseline that does not use our compositional approach. We also show that CLIS yields an average speed-up of 3.5× for individual UDFs and 1.3× to 3.1× in terms of end-to-end application performance.


Author(s):  
Alessandro Abate ◽  
Cristina David ◽  
Pascal Kesseli ◽  
Daniel Kroening ◽  
Elizabeth Polgreen

2005 ◽  
Vol 32 (4) ◽  
pp. 41-47 ◽  
Author(s):  
Annabelle McIver ◽  
Carroll Morgan

2012 ◽  
Vol 413 (1) ◽  
pp. 58-72 ◽  
Author(s):  
Suzana Andova ◽  
Sonja Georgievska ◽  
Nikola Trčka

Sign in / Sign up

Export Citation Format

Share Document