Skip to content

A prototype of soft contract verification for an untyped functional language

License

Notifications You must be signed in to change notification settings

philnguyen/soft-contract

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Build Status

Soft Contract Verifier

This is a branch of the tool that's under active development, with the main differences:

  • Writing the analysis as (a variant of) abstract definitional interpreter with an improved cache-fixing loop that reduces redundant computation.
  • Per-step abstract garbage collection with respect to a much smaller live set, thanks to stack irrelevance and big-step formulation, as well-described in Stack-Liberated Abstract Garbage Collection, although the technique was independently discovered.
  • Dropping dependence on Z3 in favor of an internal solver, as the analysis's typical use case is a large number of very simple queries.

The tool is expected to be plagued with bugs and not ready for production.

The previous versions of the implementation are archived in branches icfp14, pldi-aec-2015, jpf, popl18-ae.

Installation

Clone this repository

git clone https://github.com/philnguyen/soft-contract.git

Navigate into the inner soft-contract directory and install using raco:

cd soft-contract/soft-contract
raco pkg install --deps search-auto

Usage

To verify one or more modules, use raco scv command:

raco scv paths/to/files.rkt ...

Non-standard construct

Using non-standard constructs require fake-contract:

(require soft-contract/fake-contract)

About

A prototype of soft contract verification for an untyped functional language

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 4

  •  
  •  
  •  
  •