Model checking JAVA programs using JAVA PathFinder
From MaRDI portal
Publication:1856163
DOI10.1007/s100090050043zbMath1059.68585OpenAlexW2040060046MaRDI QIDQ1856163
Klaus Havelund, Thomas Pressburger
Publication date: 2000
Published in: International Journal on Software Tools for Technology Transfer. STTT (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/2060/20000068918
Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (20)
Model checking dynamic memory allocation in operating systems ⋮ Beyond contracts for concurrency ⋮ Optimistic synchronization-based state-space reduction ⋮ MAVEN: Modular aspect verification and interference analysis ⋮ From NuSMV to SPIN: Experiences with model checking flight guidance systems ⋮ System-level state equality detection for the formal dynamic verification of legacy distributed applications ⋮ Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving ⋮ The role of abstraction in model checking ⋮ A model checking-based approach for security policy verification of mobile systems ⋮ Symbolic predictive analysis for concurrent programs ⋮ Unnamed Item ⋮ Abstract interpretation of microcontroller code: intervals meet congruences ⋮ A dynamic logic for deductive verification of multi-threaded programs ⋮ Threaded behavior protocols ⋮ Verification of Boolean programs with unbounded thread creation ⋮ Efficient SAT-based bounded model checking for software verification ⋮ A local approach for temporal model checking of Java bytecode ⋮ Syntax-directed model checking of sequential programs ⋮ 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: Model checking JAVA programs using JAVA PathFinder
