Finding feasible counter-examples when model checking abstracted Java programs

DOI10.1007/3-540-45319-9_20MaRDI QIDQ2769593zbMATH OpenFDO

Authors Matthew B. Dwyer, Willem Visser, Corina S. Păsăreanu

Publication date 5 February 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2031/20310284

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)

Recommendations

• Model checking: from hardware to software.
• Symbolic Counter Abstraction for Concurrent Software
• Context-aware counter abstraction
• Computer Aided Verification
• scientific article; zbMATH DE number 2087636

Cited in

(11)

• Model checking JAVA programs using JAVA PathFinder
• Using runtime analysis to guide model checking of Java programs
• Combining model checking and data-flow analysis
• Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances
• Bug Hunting with False Negatives
• Symbolic Counter Abstraction for Concurrent Software
• scientific article; zbMATH DE number 2087636 (Why is no real title available?)
• Falsifying safety properties through games on over-approximating models
• Context-aware counter abstraction
• Verifying time partitioning in the DEOS scheduling kernel
• Translating Java for multiple model checkers: The Bandera back-end

Describes a project that uses

Uses Software

• SPIN
• Bandera

This page was built for publication: Finding feasible counter-examples when model checking abstracted Java programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2769593)