Inferring Canonical Register Automata
Abstract elided by the publisher.
642 papers · page 19 of 33
Software Verification with Liquid Types
Abstract elided by the publisher.
Alternating Control Flow Reconstruction
Abstract elided by the publisher.
Effective Synthesis of Asynchronous Systems from GR(1) Specifications
We consider automatic synthesis from linear temporal logic specifications for asynchronous systems. We aim the produced reactive systems to be used as software in a multi-threaded environment. We extend previous reduction of asynchronous synthesis to synchronous synthesis to the …
Sound Non-statistical Clustering of Static Analysis Alarms
Abstract elided by the publisher.
Automating Induction with an SMT Solver
Abstract elided by the publisher.
Modeling Asynchronous Message Passing for C Programs
Abstract elided by the publisher.
Local Symmetry and Compositional Verification
Abstract elided by the publisher.
Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
Abstract elided by the publisher.
versat: A Verified Modern SAT Solver
Abstract elided by the publisher.
Decision Procedures for Region Logic
Abstract elided by the publisher.
A General Framework for Probabilistic Characterizing Formulae
Abstract elided by the publisher.
Loop Invariant Symbolic Execution for Parallel Programs
Abstract elided by the publisher.
Ideal Abstractions for Well-Structured Transition Systems
Abstract elided by the publisher.
More Precise Yet Widely Applicable Cost Analysis
Abstract elided by the publisher.
Refinement-Based CFG Reconstruction from Unstructured Programs
Abstract elided by the publisher.
SAT-Based Model Checking without Unrolling
Abstract elided by the publisher.
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
Craig interpolation has emerged as an effective means of generating candidate program invariants. We present interpolation procedures for the theories of Presburger arithmetic combined with (i) uninterpreted predicates (QPA+UP), (ii) uninterpreted functions (QPA+UF) and (iii) ext…
Probabilistic Büchi Automata with Non-extremal Acceptance Thresholds
Abstract elided by the publisher.
Synthesis of Fault-Tolerant Embedded Systems Using Games: From Theory to Practice
Abstract elided by the publisher.