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

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

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

(30)

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

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)