Towards the automated verification of multithreaded Java programs

DOI10.1007/3-540-46002-0_13MaRDI QIDQ4472236zbMATH OpenFDO

Authors Giorgio Delzanno, Laurent Van Begin, Jean-François Raskin

Publication date 4 August 2004

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/2280/22800173.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A tool-supported proof system for multithreaded Java.
• An assertion-based proof system for multithreaded Java
• Model-checking multi-threaded distributed Java programs
• Constraint-based automatic verification of abstract models of multithreaded programs
• A dynamic logic for deductive verification of multi-threaded programs

Cited in

(24)

• Parameterized model checking of rendezvous systems
• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Running time analysis of broadcast consensus protocols
• Data flow analysis of asynchronous systems using infinite abstract domains
• Directed reachability for infinite-state systems
• On the \(\omega\)-language expressive power of extended Petri nets
• Expand, enlarge and check: new algorithms for the coverability problem of WSTS
• Well-structured languages
• Model-checking multi-threaded distributed Java programs
• Monotonic extensions of Petri nets: forward and backward search revisited
• Constraint-based automatic verification of abstract models of multithreaded programs
• Verifying a Compiler for Java Threads
• Proof-outlines for threads in Java
• A dynamic logic for deductive verification of multi-threaded programs
• Multi-parameterised compositional verification of safety properties
• scientific article; zbMATH DE number 7407775 (Why is no real title available?)
• Light-weight SMT-based model checking
• scientific article; zbMATH DE number 5499373 (Why is no real title available?)
• Security monitor inlining and certification for multithreaded Java
• Expressive Power of Broadcast Consensus Protocols
• Automatic WSTS-based repair and deadlock detection of parameterized systems
• Safety analysis of parameterised networks with non-blocking rendez-vous
• Decidability and complexity of decision problems for affine continuous vass
• Wait-only broadcast protocols are easier to verify

Describes a project that uses

Uses Software

• HyTech

This page was built for publication: Towards the automated verification of multithreaded Java programs

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