On the role of automated theorem proving in the compile-time derivation of concurrency

DOI10.1007/BF00244290MaRDI QIDQ1819947zbMATH OpenFDO

Authors Christian Lengauer

Publication date 1985

Published in Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

concurrencyprogram transformationautomated program synthesis and validation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Recommendations

• Verification of concurrent programs: The automata-theoretic framework
• scientific article; zbMATH DE number 3902008
• Automatic verification of concurrent systems using a formula-based compositional approach
• Automatic and hierarchical verification for concurrent systems
• Specification and verification of concurrent programs through refinements

Cited in

(5)

• scientific article; zbMATH DE number 3902008 (Why is no real title available?)
• A verification system for concurrent programs based on the Boyer-Moore prover
• A theorem prover for a computational logic
• A mechanization of unity in PC-NQTHM-92
• The automated proof of a trace transformation for a bitonic sort

This page was built for publication: On the role of automated theorem proving in the compile-time derivation of concurrency

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