Property-Directed Inference of Universal Invariants or Proving Their Absence
Abstract elided by the publisher.
2,069 papers · page 41 of 104
Deductive Program Repair
We present an approach to program repair and its application to programs with recursive functions over unbounded data types. Our approach formulates program repair in the framework of deductive synthesis that uses existing program structure as a hint to guide synthesis. We introd…
SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms
Abstract elided by the publisher.
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs
Abstract elided by the publisher.
Automatic Rootcausing for Program Equivalence Failures in Binaries
Abstract elided by the publisher.
Fine-Grained Caching of Verification Results
Abstract elided by the publisher.
Verifying Linearizability of Intel® Software Guard Extensions
Abstract elided by the publisher.
Bbs: A Phase-Bounded Model Checker for Asynchronous Programs
Abstract elided by the publisher.
The Inez Mathematical Programming Modulo Theories Framework
Abstract elided by the publisher.
An Axiomatic Specification for Sequential Memory Models
Abstract elided by the publisher.
PVSio-web 2.0: Joining PVS to HCI
Abstract elided by the publisher.
Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation
The inference and the verification of numerical relationships among variables of a program is one of the main goals of static analysis. In this paper, we propose an Abstract Interpretation framework based on higher-dimensional ellipsoids to automatically discover symbolic quadrat…
Systematic Asynchrony Bug Exploration for Android Apps
Abstract elided by the publisher.
Percentile Queries in Multi-dimensional Markov Decision Processes
Abstract elided by the publisher.
A Type-Directed Approach to Program Repair
Abstract elided by the publisher.
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT
We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided techniques for quantifi…
Alchemist: Learning Guarded Affine Functions
Abstract elided by the publisher.
OptiMathSAT: A Tool for Optimization Modulo Theories
Abstract elided by the publisher.
Predicting a Correct Program in Programming by Example
Abstract elided by the publisher.
Time-Aware Abstractions in HybridSal
Abstract elided by the publisher.