Learning to verify branching time properties

DOI10.1007/S10703-006-0026-XMaRDI QIDQ2642669zbMATH OpenOpenAlexFDO

Authors Abhay Vardhan, Mahesh Viswanathan

Publication date 17 August 2007

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2142/11092

zbMATH Keywords

CTLLearningVerification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Using language inference to verify omega-regular properties
• Modalities for model checking: Branching time logic strikes back
• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• Symbolic model checking with fewer fixpoint computations
• Quantified computation tree logic

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• Action Language Verifier, extended
• Actively learning to verify safety for FIFO automata
• Algorithmic improvements in regular model checking.
• Automated assume-guarantee reasoning for simulation conformance
• scientific article; zbMATH DE number 3660804 (Why is no real title available?)
• scientific article; zbMATH DE number 1406234 (Why is no real title available?)
• Inference of finite automata using homing sequences
• Iterating transducers in the large (extended abstract)
• Learning assumptions for compositional verification
• Learning regular sets from queries and counterexamples
• Learning to verify branching time properties
• Mining specifications
• Regular model checking
• Regular model checking using inference of regular languages
• Regular model checking using widening techniques
• Symbolic compositional verification by learning assumptions
• Tools and Algorithms for the Construction and Analysis of Systems
• TREX: A tool for reachability analysis of complex systems
• Using language inference to verify omega-regular properties
• Well-structured transition systems everywhere!
• Widening arithmetic automata

Cited in

(5)

• Learning linear temporal properties from noisy data: a MaxSAT-based approach
• Learning to verify branching time properties
• On Computability of Logical Approaches to Branching-Time Property Verification of Programs
• Using language inference to verify omega-regular properties
• Action language verifier: An infinite-state model checker for reactive software specifications

Describes a project that uses

Uses Software

• LASH
• TREX

This page was built for publication: Learning to verify branching time properties

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