scientific article; zbMATH DE number 1424030

MaRDI QIDQ4945220zbMATH OpenFDO

Authors Jesper Møller, Jakob Lichtenberg, Henrik Reif Andersen, Henrik Hulgaard

Publication date 23 March 2000

zbMATH Keywords

data structuredifference decision diagrams

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1390338
• Binary decision diagrams
• Binary decision diagrams
• Decision diagrams for verification
• Decision diagrams and dynamic programming
• Decomposition based on decision diagrams
• scientific article; zbMATH DE number 569736
• Difference graphs
• Difference graphs

Cites work

• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 2102717 (Why is no real title available?)
• Introduction to algorithms.
• Kronos: A verification tool for real-time systems
• Symbolic model checking for real-time systems
• Uppaal in a nutshell

Cited in

(23)

• On the complexities of selected satisfiability and equivalence queries over Boolean formulas and inclusion queries over hulls
• A rewriting approach to binary decision diagrams
• Zero, successor and equality in BDDs
• Symbolic model checking of timed guarded commands using difference decision diagrams
• Formal verification based on Boolean expression diagrams
• Bounded model checking for timed automata
• Model-based verification, optimization, synthesis and performance evaluation of real-time systems
• scientific article; zbMATH DE number 2088658 (Why is no real title available?)
• Binary decision diagrams
• Model Checking Real-Time Systems
• Improvements for the Symbolic Verification of Timed Automata
• Reachability analysis for timed automata using max-plus algebra
• A theoretical and numerical analysis of the worst-case size of reduced ordered binary decision diagrams
• scientific article; zbMATH DE number 2090292 (Why is no real title available?)
• scientific article; zbMATH DE number 2102717 (Why is no real title available?)
• scientific article; zbMATH DE number 1400094 (Why is no real title available?)
• A symbolic model for timed concurrent constraint programming
• An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints
• Can decision diagrams overcome state space explosion in real-time verification?
• Efficient Evaluation of Arbitrary Relational Calculus Queries
• Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods
• Explaining control policies through predicate decision diagrams
• The octagon abstract domain

Describes a project that uses

Uses Software

• Kronos
• Uppaal

This page was built for publication:

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