Skip to content

Performs static analysis on C functions to confirm equivalency using MiniZinc

Notifications You must be signed in to change notification settings

dbunker/ArchStatMzn

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

7 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

ArchStatMzn

Performs static analysis on C functions to confirm equivalancy.

These problems use MiniZinc for static analysis. Static analysis and constraint programming often use similar resolution tools designed specifically for solving potentially exponentially difficult computations.

Minisat and other CNF solvers like it are well matched for discrete computational problems, making them ideal for representing a modern CPU, however constraint programming sometimes has to venture into continuous territory possibly employing simplex and other techniques not well suited for the discrete world view.

However, this is not to say that taking a continuous approach to some static analysis problems wouldn't prove more effective. These problems experiment with this idea.

The main idea is to first take a set of problems used as a specification (input_programs labeled with -spec.c) solving for a result, then solve for the a result using the same input with a test program (input_programs labeled with -other.c) and then testing to see if there is any possible input that leads to a differing result.

Testing is performed on problems from CSAPP (http://csapp.cs.cmu.edu)

More information on MiniZinc can be found at: http://minizinc.org

About

Performs static analysis on C functions to confirm equivalency using MiniZinc

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published