Learning the Language of Error: Accessory Information
Demos
DockingApproachExample_Ext
bubble_sort_linux_false
ifstofunctions_defroster
merge_sort_false
sll_to_dll_rev_false
tcas_auto_instrumented
schedule
JQ
Usage Instructions
- Get Learn Environment
svn co https://subversion.assembla.com/svn/learn_environment/branch/pv/ pv
- Build Learn Environment
cd pv; make
- Add PV to PATH or bin directory
ln -s pv/release/pv /usr/bin
- Add libalf to LD_LIBRARY_PATH or lib directory
ln -s pv/libalf/libalf-v0.3/libalf/src/libalf.so /usr/lib
- Run on command line
pv --start-user-unwinding 1 --end-user-unwinding 1 --start-max-word-length 25
--end-max-word-length 25 --instrument-functions "Non_Crossing_Biased_Climb ALIM
Inhibit_Biased_Climb Non_Crossing_Biased_Descend Own_Below_Threat Own_Above_Threat alt_sep_test
initialize fake0 fake1" pv-test/resources/paper_demos/tcas_auto_instrumented.c --config cbmc
- 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:
Open Source Code used in Demos:
