Learning the Language of Error: Accessory Information

• Demos
• Usage instructions
• Resources

Demos

DockingApproachExample_Ext

User bound:		4
Maximum word length:		15
Zoom:		100

bubble_sort_linux_false

User bound:		2
Maximum word length:		12
Zoom:		100

ifstofunctions_defroster

User bound:		1
Maximum word length:		25
Zoom:		100

merge_sort_false

User bound:		2
Maximum word length:		7
Zoom:		100

sll_to_dll_rev_false

User bound:		2
Maximum word length:		23
Zoom:		100

tcas_auto_instrumented

User bound:		1
Maximum word length:		18
Zoom:		100

schedule

User bound:		2
Maximum word length:		4
Zoom:		100

Usage Instructions

1. Get Learn Environment

   svn co https://subversion.assembla.com/svn/learn_environment/ learn_trunk

2. Get CBMC

   svn co http://www.cprover.org/svn/cbmc/trunk/@5190 cbmc_trunk

3. Patch CBMC

   svn patch learn_trunk/trunk/cbmc-patch/learn-v3-full-cbmc-5190.diff cbmc_trunk/

4. Build CBMC As instructed in cbmc_trunk/COMPILING, per OS. For example on OSX:

   make -C cbmc_trunk/src minisat2-download
   make -C cbmc_trunk/src

5. Add CBMC, goto-cc and goto-instrument to path or move to bin

   ln -s cbmc_trunk/src/cbmc/cbmc /usr/bin
   ln -s cbmc_trunk/src/goto-cc/goto-cc /usr/bin
   ln -s cbmc_trunk/src/goto-instrument/goto-instrument /usr/bin

6. (optional) If on a Windows OS, enable makefile

   mv Makefile Makefile.linux
   mv Makefile.win Makefile

7. Build learn environment

   make -C learn_trunk/trunk/

8. Run GUI (for command line skip to Step 11.)

   cd learn_trunk/trunk/
   java -jar gui.jar

9. Press 'Select File' and navigate to 'learn_trunk/trunk/paper_demos/tcas_auto_instrumented/tcas_auto_instrumented.c'
10. Press 'Run'
11. (optional) Run on command line

    cd learn_trunk/trunk/
    ./run.sh paper_demos/tcas_auto_instrumented/tcas_auto_instrumented.c

Contact

• Martin Chapman, Department of Informatics, King's College London, UK
• Hana Chockler, Department of Informatics, King's College London, UK
• Pascal Kesseli, Department of Computer Science, University of Oxford, UK
• Daniel Kroening, Department of Computer Science, University of Oxford, UK
• Ofer Strichman, Information Systems Engineering, Technion, Haifa, Israel
• Michael Tautschnig, EECS, Queen Mary University of London, UK

Resources

All automata in .dot, .svg and .png format:

• DockingApproachExample_Ext.tar.gz
• bubble_sort_linux_false.tar.gz
• ifstofunctions_defroster.tar.gz
• merge_sort_false.tar.gz
• sll_to_dll_rev_false.tar.gz
• tcas_auto_instrumented.tar.gz
• schedule.tar.gz

Open Source Code used in Demos:

• DockingApproachExample_Ext_Code (original)
  • Original source project.
• DockingApproachExample_Ext_Code (goto)
  • Full project merged into a single, CBMC-compatible source file.
• bubble_sort_linux_false
• ifstofunctions_defroster
• merge_sort_false
• sll_to_dll_rev_false
• tcas_auto_instrumented
• schedule