State/Event Software Verification for Branching-Time Specifications

DOI10.1007/11589976_5MaRDI QIDQ5429308zbMATH OpenOpenAlexFDO

Authors Sagar Chaki, Orna Grumberg, Joël Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith, Edmund Clarke

Publication date 29 November 2007

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

Full work available at URL https://doi.org/10.1007/11589976_5

zbMATH Keywords

Automated Abstraction RefinementBranching-time Temporal LogicConcurrent Software Model CheckingState/Event-based Verification

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

• Integrated Formal Methods
• Concurrent software verification with states, events, and deadlocks
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Verification of large state/event systems using compositionality and dependency analysis
• Software model checking

Cited in

(5)

• Compositional verification and 3-valued abstractions join forces
• Temporal property verification as a program analysis task
• Efficient CTL verification via Horn constraints solving
• A rewriting-based model checker for the linear temporal logic of rewriting
• Integrated Formal Methods

Describes a project that uses

Uses Software

• ComFoRT
• MAGIC

This page was built for publication: State/Event Software Verification for Branching-Time Specifications

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