Scribd
Upload
65 views12 pages

Design Compiler Verification

This document discusses designing a verifying compiler. It describes tools like ESC/Java and Spec# that perform verification by checking specifications at compile time. ESC/Java checks for runtime errors while Spec# extends type systems and emits runtime checks. The document also discusses advantages of pre-verification, how to verify loops and arrays, type checking separately from verification, and approaches like testing and formal methods for verification.

Uploaded by

Umer Sabir
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PPTX, PDF, TXT or read online on Scribd
65 views12 pages

Design Compiler Verification

This document discusses designing a verifying compiler. It describes tools like ESC/Java and Spec# that perform verification by checking specifications at compile time. ESC/Java checks for runtime errors while Spec# extends type systems and emits runtime checks. The document also discusses advantages of pre-verification, how to verify loops and arrays, type checking separately from verification, and approaches like testing and formal methods for verification.

Uploaded by

Umer Sabir
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PPTX, PDF, TXT or read online on Scribd
You are on page 1/ 12

Designing a

Verifying compiler
Group Members

 Muhammad Umer (CS141002)


 Ameer Hamza(CS141050)
 Zeeshan Mumtaz(CS141051)
Abstract

 Development of a tool which automatically verifies programs


meet their specifications, and are free from runtime errors such
as divide-by-zero, array out-of-bounds and null dereferences.
 It should be a pre-compiler phase of any compiler which checks
the verification of code.
 Pre-Processing Verification includes Syntax and Semantics
checks.
Overview

 Several impressive systems have been developed to this end,


such as ESC/Java and Spec#, which build on existing
programming languages (e.g., Java, C#).
 ESC/Java (and more recently ESC/Java2), the "Extended Static
Checker for Java," is a programming tool that attempts to find
common run-time errors in java programs at compile time.
ESC/Java

 For example, that an integer variable is greater-than-zero, or lies


between the bounds of an array. This technique was pioneered in
ESC/Java (and its predecessor, ESC/Modula-3) and can be thought
of as an extended form of type checking.
 It checks all the language specifications which are necessary for
the program to run free from run-time errors.
Spec#

 Spec#(Spec Sharp) extends the type system to include non-null


types and checked exceptions.
 The compiler statically enforces non-null types, emits run-time
checks for method contracts and invariants, and records the
contracts as metadata for consumption by downstream tools.
  It uses an automatic theorem prover that analyzes the
verification conditions to prove the correctness of the program or
find errors in it.
Advantages of Pre-verify Compiler

 The entire program is verified so there are no syntax or semantic


errors.
 The executable file is optimized by the compiler so it execute
faster.
 User do not have to execute the program on the same machine it
was built.
Example

function decrement(int x)->(int y)


//Parameter x must be greater than zero
Requires x>0
//Return must be greater or equal to zero
Ensures y>=0:
//
returnx-1
How to verify Loops And Arrays

Function sum(int[]items)->(int r)
Requires all {iin0..|items||items[i]>=0}
Ensures r>=0:
//
Int i=0
Int r=0
While i<|items|where i>=0&&r>=0:
r=r+items[i]
i=i+1
Return r
Type checking is separate from
verification
Function f(int|null x)->bool|null:
//
If x is int && x>=0:
Return true
Else if x is int &&x<0:
Return false
else:
Return x
Verification Approaches

Testing-based approach
 Test and validation suite to verify compilers
 Test suite to qualify the compiler’s output
Formal method-based approach
 Formal verification of compilers
 Formal verification of compiler’s output.
 Translation validation to check the correctness of the compilation
Conclusion

 In this presentation we have talk about two language


specification tools (ESC/JAVA, Spec#) but there are lot more tools
that are working on the same project like (Dafny, VeriFast, Why3
and Frama C).

You might also like