Coqoon - An IDE for Interactive Proof Development in Coq
International audience
1,553 papers · page 35 of 78
Diagnostic Information for Control-Flow Analysis of Workflow Graphs (a.k.a. Free-Choice Workflow Nets)
Abstract elided by the publisher.
CPA-BAM: Block-Abstraction Memoization with Value Analysis and Predicate Analysis - (Competition Contribution)
Abstract elided by the publisher.
Interpolants in Nonlinear Theories Over the Reals
Abstract elided by the publisher.
An O(m\log n) Algorithm for Stuttering Equivalence and Branching Bisimulation
We provide a new algorithm to determine stuttering equivalence with time complexity $$Om \log n$$, where n is the number of states and m is the number of transitions of a Kripke structure. This algorithm can also be used to determine branching bisimulation in $$Om\log | Act |+\lo…
Tactics for the Dafny Program Verifier
Abstract elided by the publisher.
Vienna Verification Tool: IC3 for Parallel Software - (Competition Contribution)
Abstract elided by the publisher.
Ultimate Automizer with Two-track Proofs - (Competition Contribution)
Abstract elided by the publisher.
Run Forester, Run Backwards! - (Competition Contribution)
Abstract elided by the publisher.
Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems
Abstract elided by the publisher.
PrDK: Protocol Programming with Automata
Abstract elided by the publisher.
Safety-Constrained Reinforcement Learning for MDPs
We consider controller synthesis for stochastic and partially unknown environments in which safety is essential. Specifically, we abstract the problem as a Markov decision process in which the expected performance is measured using a cost function that is unknown prior to run-tim…
LPI: Software Verification with Local Policy Iteration - (Competition Contribution)
Abstract elided by the publisher.
PTIME Computation of Transitive Closures of Octagonal Relations
Computing transitive closures of integer relations is the key to finding precise invariants of integer programs. In this paper, we study difference bounds and octagonal relations and prove that their transitive closure is a PTIME-computable formula in the existential fragment of …
Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark - (Competition Contribution)
Abstract elided by the publisher.
PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games
Abstract elided by the publisher.
Characteristic Formulae for Session Types
Subtyping is a crucial ingredient of session type theory and its applications, notably to programming language implementations. In this paper, we study effective ways to check whether a session type is a subtype of another by applying a characteristic formulae approach to the pro…
Online and Compositional Learning of Controllers with Application to Floor Heating
Abstract elided by the publisher.
Developing and Debugging Proof Strategies by Tinkering
Abstract elided by the publisher.
Abstract Learning Frameworks for Synthesis
We develop abstract learning frameworks for synthesis that embody the principles of the CEGIS counterexample-guided inductive synthesis algorithms in current literature. Our framework is based on iterative learning from a hypothesis space that captures synthesized objects, using …