Using runtime analysis to guide model checking of Java programs
From MaRDI portal
concurrent programsdeadlocksguided model checkingJavaprogram verificationrace conditionsruntime analysis
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)
Recommendations
- Model checking JAVA programs using JAVA PathFinder
- scientific article; zbMATH DE number 2087636
- Java Memory Model-Aware Model Checking
- Faster and more complete extended static checking for the Java modeling language
- Automated Technology for Verification and Analysis
- Finding feasible counter-examples when model checking abstracted Java programs
Cited in
(13)- A local approach for temporal model checking of Java bytecode
- Model checking JAVA programs using JAVA PathFinder
- An overview of the runtime verification tool Java PathExplorer
- Automated formal analysis and verification: an overview
- Java Memory Model-Aware Model Checking
- Runtime Exception Detection in Java Programs Using Symbolic Execution
- Program visualization for debugging deadlocks in multithreaded programs
- Effect-polymorphic behaviour inference for deadlock checking
- Deadlock checking by data race detection
- scientific article; zbMATH DE number 2102730 (Why is no real title available?)
- HyperMonitor: a Python prototype for hyper predictive runtime verification
- Collecting statistics over runtime executions
- On the complexity of partial order trace model checking
This page was built for publication: Using runtime analysis to guide model checking of Java programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2753764)
