Name
Abstract | ||
|---|---|---|
This is an attempt to combine the two research areas of programming methodology and automated theorem proving. We investigate the potential for automation of a programming methodology that supports the compile-time derivation of concurrency in imperative programs. In this methodology, concurrency is identified by the declaration of certain semantic properties (so-called "semantic relations") of appropriate program parts. Semantic declarations can be exploited to transform the sequential execution of the program into a parallel execution. We make observations about the automation of correctness proofs of such transformations for a limited domain of programs: sorting networks. |
Year | DOI | Venue |
|---|---|---|
1984 | 10.1007/3-540-15670-4_7 | Seminar on Concurrency |
Keywords | Field | DocType |
static derivation,mechanzed certification,sorting network,automated theorem proving | Programming language,Computer science,Concurrency,Automated theorem proving,Semantic property,Automated proof checking,Theoretical computer science,Automation,Software development process,Program derivation,Proof complexity | Conference |
Volume | ISSN | ISBN |
197 | 0302-9743 | 3-540-15670-4 |
Citations | PageRank | References |
3 | 0.73 | 10 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christian Lengauer | 1 | 1738 | 117.05 |
| Chua-huang Huang | 2 | 281 | 35.34 |