JAR 2008 - PDF Preprint Papers

JAR 2008

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed JAR-2008 Paper

click to vote

JAR
2008

124views more JAR 2008»

Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations

14 years 12 days ago

Download cristal.inria.fr

This article presents the formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C and compiler intermediate languages. Be...

Xavier Leroy, Sandrine Blazy

claim paper

Read More »

Disclaimer and Copyright Notice

Sciweavers respects the rights of all copyright holders and in this regard, authors are only allowed to share a link to their preprint paper on their own website. Every contribution is associated with a desciptive image. It is the sole responsibility of the authors to ensure that their posted image is not copyright infringing. This service is compliant with IEEE copyright.

Id	Views	Title	Status

1	124	Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations	claim
2	115	Formal Models and Analysis of Secure Multicast in Wired and Wireless Networks	claim
3	107	Differential Dynamic Logic for Hybrid Systems	claim
4	105	Proof Synthesis and Reflection for Linear Arithmetic	claim
5	101	Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves	claim
6	98	A Mechanical Analysis of Program Verification Strategies	claim
7	95	On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic	claim
8	89	An Extensible Encoding of Object-oriented Data Models in hol	claim
9	88	Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables	claim
10	81	Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints	claim
11	81	Automatic Symmetry Detection for Promela	claim
12	77	Translating Higher-Order Clauses to First-Order Clauses	claim
13	77	Data Complexity of Query Answering in Expressive Description Logics via Tableaux	claim
14	70	Assumption-Commitment Support for CSP Model Checking	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers