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)

Full work available at URL https://doi.org/10.1007/BF00244290

zbMATH Keywords

automated program synthesis and validationconcurrencyprogram transformation

Mathematics Subject Classification ID

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

Review text

A recent trend in program development is to derive correct implementations from program specifications by the application of a formal calculus, a programming methodology. The application of formal rules lends itself to automation. We investigate the automation of one part of a methodology for programming with concurrency. In this methodology, concurrency is derived by transforming the sequential execution of a program into an equivalent concurrent execution on the basis of formal transformation rules. Such rules can be interpreted as theorems of semantic equivalences. The mechanical certification of these theorems would significantly enhance the reliability of the methodology. The following is an initial exploration of this problem applied to a certain class of programs: sorting networks. We present an implementation of a part of the underlying semantic theory in Boyer and Moore's mechanized logic, and report on the mechanical proof of a transformation that derives concurrency for an insertion sort.

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

(6)

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

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)