Are the logical foundations of verifying compiler prototypes matching user expectations?

DOI10.1007/s00165-006-0016-1zbMath1121.68025OpenAlexW2127225601WikidataQ121712811 ScholiaQ121712811MaRDI QIDQ2643125

Patrice Chalin

Publication date: 23 August 2007

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-006-0016-1

zbMATH Keywords

SurveyLogical foundationsRuntime assertion checkingAssertionsDesign by contractExtended static checkingIndustrial practiceStatic program verification

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Related Items (1)

Efficient Well-Definedness Checking

Uses Software

• Ada95
• LARCH
• SPARK
• KRAKATOA
• Visual C#
• Eiffel
• JML
• Spec#
• ESC/Java
• KeY
• LOOP
• Splint
• LCLint
• Jass

Cites Work

• SPARK
• A logic covering undefinedness in program proofs
• A typed logic of partial functions reconstructed classically
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Writing Larch interface language specifications
• Two over three: a two-valued logic for software specification and validation over a three-valued predicate calculus
• Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Are the logical foundations of verifying compiler prototypes matching user expectations?