Abstraction-Based Interaction Model for Synthesis
Abstract elided by the publisher.
642 papers · page 11 of 33
Generating Tests by Example
Abstract elided by the publisher.
A Logical System for Modular Information Flow Verification
Abstract elided by the publisher.
On Constructivity of Galois Connections
Abstract elided by the publisher.
Revisiting MITL to Fix Decision Procedures
Metric Interval Temporal Logic ( MITL ) is a well studied real-time, temporal logic that has decidable satisfiability and model checking problems. The decision procedures for MITLrely on the automata theoretic approach, where logic formulas are translated into equivalent timed au…
Selfless Interpolation for Infinite-State Model Checking
Abstract elided by the publisher.
An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
Abstract elided by the publisher.
P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols
Abstract elided by the publisher.
Partitioned Memory Models for Program Analysis
Abstract elided by the publisher.
Effective Bug Finding in C Programs with Shape and Effect Abstractions
Abstract elided by the publisher.
Bringing LTL Model Checking to Biologists
The BioModelAnalyzer (BMA) is a web based tool for the development of discrete models of biological systems. Through a graphical user interface, it allows rapid development of complex models of gene and protein interaction networks and stability analysis without requiring users t…
Structuring Abstract Interpreters Through State and Value Abstractions
Abstract elided by the publisher.
Synthesizing Non-Vacuous Systems
Abstract elided by the publisher.
Static Analysis of Communicating Processes Using Symbolic Transducers
Abstract elided by the publisher.
Reduction of Workflow Nets for Generalised Soundness Verification
Abstract elided by the publisher.
Matching Multiplications in Bit-Vector Formulas
Bit-vector formulas arising from hardware verification problems often contain word-level arithmetic operations. Empirical evidence shows that state-of-the-art SMT solvers are not very efficient at reasoning about bit-vector formulas with multiplication. This is particularly true …
Detecting Strict Aliasing Violations in the Wild
Abstract elided by the publisher.
Independence Abstractions and Models of Concurrency
Abstract elided by the publisher.
Complete Abstractions and Subclassical Modal Logics
Abstract elided by the publisher.
Using Abstract Interpretation to Correct Synchronization Faults
Abstract elided by the publisher.