AVATAR: The Architecture for First-Order Theorem Provers
Abstract elided by the publisher.
2,069 papers · page 45 of 104
GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components
Abstract elided by the publisher.
Learning Universally Quantified Invariants of Linear Data Structures
We propose a new automaton model, called quantified data automata over words, that can model quantified invariants over linear data structures, and build poly-time active learning algorithms for them, where the learner is allowed to query the teacher with membership and equivalen…
Relative Equivalence in the Presence of Ambiguity
Abstract elided by the publisher.
Recursive Program Synthesis
Abstract elided by the publisher.
Beautiful Interpolants
Abstract elided by the publisher.
Partial Orders for Efficient Bounded Model Checking of Concurrent Software
Abstract elided by the publisher.
Automatic Generation of Quality Specifications
Abstract elided by the publisher.
PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems
Abstract elided by the publisher.
SVA and PSL Local Variables - A Practical Approach
Abstract elided by the publisher.
DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs
Abstract elided by the publisher.
Solving Existentially Quantified Horn Clauses
Abstract elided by the publisher.
Distributed Explicit State Model Checking of Deadlock Freedom
Abstract elided by the publisher.
QUAIL: A Quantitative Security Analyzer for Imperative Code
Abstract elided by the publisher.
Formal Verification of Hardware Synthesis
We report on the implementation of a certified compiler for a high-level hardware description language (HDL) called Fe-Si (FEatherweight SynthesIs). Fe-Si is a simplified version of Bluespec, an HDL based on a notion of guarded atomic actions. Fe-Si is defined as a dependently ty…
PRALINE: A Tool for Computing Nash Equilibria in Concurrent Games
Abstract elided by the publisher.
Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking
Abstract elided by the publisher.
Better Termination Proving through Cooperation
Abstract elided by the publisher.
Efficient Synthesis for Concurrency by Semantics-Preserving Transformations
Abstract elided by the publisher.
Combining Relational Learning with SMT Solvers Using CEGAR
Abstract elided by the publisher.