enter search term and/or author name
Through the use of conditional compilation and related tools, many software projects can be used to generate a huge number of related programs. The problem of typing such variational software is difficult. The brute-force strategy of generating...
Æminium: A Permission-Based Concurrent-by-Default Programming Language Approach
Sven Stork, Karl Naden, Joshua Sunshine, Manuel Mohr, Alcides Fonseca, Paulo Marques, Jonathan Aldrich
Article No.: 2
Writing concurrent applications is extremely challenging, not only in terms of producing bug-free and maintainable software, but also for enabling developer productivity. In this article we present the Æminium concurrent-by-default...
Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations
Hongjin Liang, Xinyu Feng, Ming Fu
Article No.: 3
Verifying program transformations usually requires proving that the resulting program (the target) refines or is equivalent to the original one (the source). However, the refinement relation between individual sequential threads cannot be...
Formal Verification of an SSA-Based Middle-End for CompCert
Gilles Barthe, Delphine Demange, David Pichardie
Article No.: 4
CompCert is a formally verified compiler that generates compact and efficient code for a large subset of the C language. However, CompCert foregoes using SSA, an intermediate representation employed by many compilers that enables writing simpler,...