Model-checking view-based partial specifications

DOI10.1016/S1571-0661(04)80962-9MaRDI QIDQ4917056zbMATH OpenFDO

Authors Michael Huth, Shekhar Pradhan

Publication date 26 April 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S1571-0661(04)80962-9

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Consistent partial model checking
• Constructive consistency checking for partial specification in Z
• Partial model checking via abstract interpretation
• scientific article; zbMATH DE number 2102712
• Model Checking for Action Abstraction

Cites work

• A typed logic of partial functions reconstructed classically
• Automatic verification methods for finite state systems. International workshop, Grenoble, France, June 12-14, 1989. Proceedings
• E3: A logic for reasoning equationally in the presence of partiality
• scientific article; zbMATH DE number 1693039 (Why is no real title available?)
• scientific article; zbMATH DE number 1696879 (Why is no real title available?)
• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 3635472 (Why is no real title available?)
• scientific article; zbMATH DE number 1759610 (Why is no real title available?)
• scientific article; zbMATH DE number 1863177 (Why is no real title available?)
• scientific article; zbMATH DE number 2102712 (Why is no real title available?)
• scientific article; zbMATH DE number 783754 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Institutions: abstract model theory for specification and programming
• Temporal abstract interpretation
• Using powerdomains to generalize relational databases
• Verifying safety properties of concurrent Java programs using 3-valued logic

Cited in

(5)

• Dealing with incompleteness in automata-based model checking
• Consistent partial model checking
• Algebraic Methodology and Software Technology
• On model checking multiple hybrid views
• Partial model checking via abstract interpretation

Describes a project that uses

Uses Software

• Alloy
• Alcoa

This page was built for publication: Model-checking view-based partial specifications

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