Effective Bug Finding in C Programs with Shape and Effect Abstractions
Abstract elided by the publisher.
26,098 papers · page 490 of 1,305
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.
Property Directed Reachability for Proving Absence of Concurrent Modification Errors
Abstract elided by the publisher.
Stabilizing Floating-Point Programs Using Provenance Analysis
Abstract elided by the publisher.
Dynamic Reductions for Model Checking Concurrent Software
Symbolic model checking of parallel programs stands and falls with effective methods of dealing with the explosion of interleavings. We propose a dynamic reduction technique to avoid unnecessary interleavings. By extending Lipton’s original work with a notion of bisimilarity, we …
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
2.5 player parity games combine the challenges posed by 2.5 player reachability games and the qualitative analysis of parity games. These two types of problems are best approached with different types of algorithms: strategy improvement algorithms for 2.5 player reachability game…
Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Abstract elided by the publisher.
Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT
Abstract elided by the publisher.
Solving Nonlinear Integer Arithmetic with MCSAT
Abstract elided by the publisher.
Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Abstract elided by the publisher.
Efficient Elimination of Redundancies in Polyhedra by Raytracing
Abstract elided by the publisher.