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

DOI10.1007/BF00244290zbMATH Open0614.68067MaRDI QIDQ1819947FDOQ1819947

Authors: Christian Lengauer 

Publication date: 1985

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

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

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)

Cited In (5)

• Title not available (Why is that?)
• A theorem prover for a computational logic
• A verification system for concurrent programs based on the Boyer-Moore prover
• 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)