scientific article
From MaRDI portal
Publication:2769592
zbMath0978.68540MaRDI QIDQ2769592
Thomas Ball, Andreas Podelski, Sriram K. Rajamani
Publication date: 5 February 2002
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2031/20310268
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Infinite-state invariant checking with IC3 and predicate abstraction ⋮ Software Verification with PDR: An Implementation of the State of the Art ⋮ Whale: An Interpolation-Based Algorithm for Inter-procedural Verification ⋮ SAT-Based Model Checking ⋮ Abstraction and Abstraction Refinement ⋮ Interpolation and Model Checking ⋮ Predicate Abstraction for Program Verification ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Symbolic Trajectory Evaluation ⋮ Symbolic perimeter abstraction heuristics for cost-optimal planning ⋮ Data structures for symbolic multi-valued model-checking ⋮ Deciding program properties via complete abstractions on bounded domains ⋮ A unifying view on SMT-based software verification ⋮ Efficient strategies for CEGAR-based model checking ⋮ A divide-and-conquer approach for analysing overlaid data structures ⋮ Syntax-guided synthesis for lemma generation in hardware model checking ⋮ Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions ⋮ Calculational design of a regular model checker by abstract interpretation ⋮ Experience of improving the BLAST static verification tool ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ CPBPV: a constraint-programming framework for bounded program verification ⋮ Abstractions of data types ⋮ Lost in abstraction: monotonicity in multi-threaded programs ⋮ Trading Plaintext-Awareness for Simulatability to Achieve Chosen Ciphertext Security ⋮ Internal and External Logics of Abstract Interpretations ⋮ Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference ⋮ Sound and Complete Abstract Graph Transformation ⋮ Cross-Checking - Enhanced Over-Approximation of the Reachable Global State Space of Component-Based Systems ⋮ On finite-state approximants for probabilistic computation tree logic ⋮ Automated formal analysis and verification: an overview ⋮ Verifying time partitioning in the DEOS scheduling kernel
Uses Software
