scientific article; zbMATH DE number 1956470

MaRDI QIDQ4417801zbMATH OpenFDO

Authors Tony Hoare

Publication date 30 July 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2622/26220262.htm

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Computing methodologies and applications (68U99)

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• The verified software repository: a step towards the verifying compiler
• Compiling a 50-year journey
• A mini challenge: build a verifiable filesystem
• A Completely Verified Realistic Bootstrap Compiler

Cited in

(31)

• Mechanising a formal model of flash memory
• POSIX file store in Z/Eves: An experiment in the verified software repository
• Algorithm design through the optimization of reuse-based generation
• Verifying Whiley programs with Boogie
• A Petri net approach for the design and analysis of web services choreographies
• The verified software repository: a step towards the verifying compiler
• Generating all polynomial invariants in simple loops
• Are the logical foundations of verifying compiler prototypes matching user expectations?
• Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems
• A mini challenge: build a verifiable filesystem
• Specification and verification challenges for sequential object-oriented programs
• scientific article; zbMATH DE number 6708298 (Why is no real title available?)
• Formalizing a hierarchical file system
• Towards ``mouldable code via nested code graph transformation
• Refactoring and representation independence for class hierarchies
• Formalizing a hierarchical file system
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
• Model checking RAISE applicative specifications
• scientific article; zbMATH DE number 7440191 (Why is no real title available?)
• POPLMark reloaded: mechanizing proofs by logical relations
• Verified Compilation and the B Method: A Proposal and a First Appraisal
• A verifiable SSA program representation for aggressive compiler optimization
• Robin Milner 1934--2010
• Verifying an Open Compiler Using Multi-language Semantics
• A Completely Verified Realistic Bootstrap Compiler
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 7774275 (Why is no real title available?)
• A correctness and incorrectness program logic
• Generation of correctness conditions for imperative programs
• Using formal reasoning on a model of tasks for FreeRTOS

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4417801)