Lazy abstraction
From MaRDI portal
Publication:5178898
DOI10.1145/503272.503279zbMath1323.68374OpenAlexW2295903414MaRDI QIDQ5178898
Ranjit Jhala, Grégoire Sutre, Rupak Majumdar, Thomas A. Henzinger
Publication date: 17 March 2015
Published in: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/503272.503279
Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (79)
Configurable verification of timed automata with discrete variables ⋮ Lazy Reachability Checking for Timed Automata with Discrete Variables ⋮ Infinite-state invariant checking with IC3 and predicate abstraction ⋮ Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic ⋮ Whale: An Interpolation-Based Algorithm for Inter-procedural Verification ⋮ Counterexample-guided predicate abstraction of hybrid systems ⋮ Abstraction and Abstraction Refinement ⋮ Predicate Abstraction for Program Verification ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Verification of Hybrid Systems ⋮ Lazy slicing for state-space exploration ⋮ Verifying distributed real-time properties of embedded systems via graph transformations and model checking ⋮ Program verification with interacting analysis plugins ⋮ LCTD: test-guided proofs for C programs on LLVM ⋮ Reusing predicate precision in value analysis ⋮ A lazy approach to symmetry reduction ⋮ Closure properties and complexity of rational sets of regular languages ⋮ Hybrid automata-based CEGAR for rectangular hybrid systems ⋮ Verification Modulo theories ⋮ Finding and fixing faults ⋮ Verifying Heap-Manipulating Programs in an SMT Framework ⋮ Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction ⋮ Dynamic Reductions for Model Checking Concurrent Software ⋮ Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis ⋮ Probabilistic CEGAR ⋮ Linear Arithmetic with Stars ⋮ A unifying view on SMT-based software verification ⋮ Efficient strategies for CEGAR-based model checking ⋮ Predicate Abstraction in Program Verification: Survey and Current Trends ⋮ Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning ⋮ An automatic method for the dynamic construction of abstractions of states of a formal model ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Verification of evolving software via component substitutability analysis ⋮ Lazy Abstraction-Based Controller Synthesis ⋮ Counterexample-Guided Refinement of Template Polyhedra ⋮ On model checking multiple hybrid views ⋮ Component-wise incremental LTL model checking ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ SMT-based model checking for recursive programs ⋮ Loop summarization using state and transition invariants ⋮ Deduction as an Engineering Science ⋮ An efficient approach for abstraction-refinement in model checking ⋮ Unnamed Item ⋮ Experience of improving the BLAST static verification tool ⋮ Convex Invariant Refinement by Control Node Splitting: a Heuristic Approach ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ A framework for computing finite SLD trees ⋮ A new representation and associated algorithms for generalized planning ⋮ Sharpening constraint programming approaches for bit-vector theory ⋮ Verifying Multithreaded Recursive Programs with Integer Variables ⋮ Generating models of infinite-state communication protocols using regular inference with abstraction ⋮ A local approach for temporal model checking of Java bytecode ⋮ Complexity and Algorithms for Monomial and Clausal Predicate Abstraction ⋮ An Assume Guarantee Approach for Checking Quantified Array Assertions ⋮ An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures ⋮ Invariant Synthesis for Combined Theories ⋮ A Forward-Backward Abstraction Refinement Algorithm ⋮ Proving Safety with Trace Automata and Bounded Model Checking ⋮ Verifying Reference Counting Implementations ⋮ Translating Xd-C programs to MSVL programs ⋮ Accelerating Interpolation-Based Model-Checking ⋮ Automatically Refining Abstract Interpretations ⋮ Refinement-Based CFG Reconstruction from Unstructured Programs ⋮ Automata Learning with Automated Alphabet Abstraction Refinement ⋮ Distributed and Predictable Software Model Checking ⋮ Abstraction refinement and antichains for trace inclusion of infinite state systems ⋮ Under-approximating loops in C programs for fast counterexample detection ⋮ Could We Have Chosen a Better Loop Invariant or Method Contract? ⋮ Abstraction Refinement for Quantified Array Assertions ⋮ Refinement of Trace Abstraction ⋮ A Configurable CEGAR Framework with Interpolation-Based Refinements ⋮ Falsifying Safety Properties Through Games on Over-approximating Models ⋮ Refining abstract interpretations ⋮ Reducing concurrent analysis under a context bound to sequential analysis ⋮ Theory decision by decomposition ⋮ Automated formal analysis and verification: an overview ⋮ Specification and verification of concurrent programs through refinements ⋮ Verifying time partitioning in the DEOS scheduling kernel ⋮ Translating Java for multiple model checkers: The Bandera back-end
Uses Software
This page was built for publication: Lazy abstraction
