Sketching synthesis technique in Spec#
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
Boogie
SpecSharp
Tests
README

README

Sketch#: Sketching in Spec#

This tool is a fork from: 
    Boogie v54898 (http://boogie.codeplex.com/)
    SpecSharp v54900 (http://specsharp.codeplex.com/)


BUILD INSTRUCTIONS
------------------

A. Builld SscSharp [* Run as Admin ]

   cd $SKETCH#\SpecSharp\SpecSharp\Microsoft.SpecSharp\LastKnownGood9
   clean.cmd
   RegisterLKG.cmd

   cd $SKETCH#\SpecSharp\SpecSharp
   devenv SpecSharp.sln /build DebugCommandLine
   devenv SpecSharp.sln /build Debug

B. Build Boogie/SscBoogie

   cd $SKETCH#\Boogie\Binaries
   nmake
   cd ..\Source
   devenv Boogie.sln /build Debug
   cd ..\..\SpecSharp\SscBoogie\Binaries
   nmake
   cd ..\Source
   devenv SscBoogie.sln /build Debug
   cd ..\Binaries
   nmake register

COMPILING INSTRUCTIONS
----------------------

$SKETCH#\Boogie\Binaries\ssc.exe /debug+ <FILENAME>.ssc

    * Notes: 
      
        /debug+ is required!

SKETCHING INSTRUCTIONS
----------------------

$SKETCH#\SpecSharp\SscBoogie\Binaries\SscBoogie.exe /sketch <Options> <FILENAME>.exe

    * Notes: 
      
        /sketch is required!

    * Attributes on method declarations:
        
        [Inline]	    : inlines body (same holes on each instance)
        [Inline][Generator] : inlines body (fresh holes on each instance)

    * Options:

        /proverLog:C:\Temp\z3-@PROC@

            store Z3 call logs for various sketching steps for debugging
        
        /traceSketch

            print sketching related debug info
    
        /numCEGARItrs:N        

            MAX number of CEGAR based synthesis iterations (default = 10)

        /numRandInpGen:N       

            number of random tuples for CEGAR synthesis (default = 1)

	/intBits:N
	
	    bit width for integer holes (allowed = {8, 16, 32}, default = 8)
	
        /numThreads:N

            runs Parallel Z3 with N threads (default = 0)

	/unboundRandInpArrLen

            do not impose implicit array length bound (= 10) when generating random arrays as input

CONTACT
------------------
Please send mail to Hesam Samimi (hesam@ucla.edu) if there are any problems