The lang/spin port
spin-6.4.7p0 – tool for formal verification of parallel software (cvsweb github mirror)
Description
Spin is a software verification tool for analyzing the consistency of asynchronous systems. Examples of asynchronous systems include multi-threaded programs, distributed systems, and communications protocols. Spin takes a system model specified in Promela (the PROcess MEta LAnguage). It also takes a specifciation of the requirements for logical correctness, and allows both interactive and exhaustive simulations of the system for verifying these properties.WWW: https://spinroot.com/
Maintainer
Ori Bernstein
Categories
Files
- /usr/local/bin/spin
- /usr/local/man/man1/spin.1
- /usr/local/share/examples/spin/
- /usr/local/share/examples/spin/Book_1991/
- /usr/local/share/examples/spin/Book_1991/App.F.datalink.h
- /usr/local/share/examples/spin/Book_1991/App.F.defines.h
- /usr/local/share/examples/spin/Book_1991/App.F.flow_cl.h
- /usr/local/share/examples/spin/Book_1991/App.F.fserver.h
- /usr/local/share/examples/spin/Book_1991/App.F.pftp.pml
- /usr/local/share/examples/spin/Book_1991/App.F.present.h
- /usr/local/share/examples/spin/Book_1991/App.F.session.h
- /usr/local/share/examples/spin/Book_1991/App.F.user.h
- /usr/local/share/examples/spin/Book_1991/README.txt
- /usr/local/share/examples/spin/Book_1991/p101.pml
- /usr/local/share/examples/spin/Book_1991/p102.pml
- /usr/local/share/examples/spin/Book_1991/p104.1.pml
- /usr/local/share/examples/spin/Book_1991/p104.2.pml
- /usr/local/share/examples/spin/Book_1991/p105.1.pml
- /usr/local/share/examples/spin/Book_1991/p105.2.pml
- /usr/local/share/examples/spin/Book_1991/p107.pml
- /usr/local/share/examples/spin/Book_1991/p108.pml
- /usr/local/share/examples/spin/Book_1991/p116.pml
- /usr/local/share/examples/spin/Book_1991/p117.pml
- /usr/local/share/examples/spin/Book_1991/p123.pml
- /usr/local/share/examples/spin/Book_1991/p248.pml
- /usr/local/share/examples/spin/Book_1991/p312.pml
- /usr/local/share/examples/spin/Book_1991/p319.pml
- /usr/local/share/examples/spin/Book_1991/p320.pml
- /usr/local/share/examples/spin/Book_1991/p325.test.h
- /usr/local/share/examples/spin/Book_1991/p327.upper.h
- /usr/local/share/examples/spin/Book_1991/p329.pml
- /usr/local/share/examples/spin/Book_1991/p330.pml
- /usr/local/share/examples/spin/Book_1991/p337.defines2.h
- /usr/local/share/examples/spin/Book_1991/p337.fserver.h
- /usr/local/share/examples/spin/Book_1991/p337.pftp.ses.pml
- /usr/local/share/examples/spin/Book_1991/p337.session.h
- /usr/local/share/examples/spin/Book_1991/p337.user.h
- /usr/local/share/examples/spin/Book_1991/p342.pftp.ses1.h
- /usr/local/share/examples/spin/Book_1991/p343.claim.h
- /usr/local/share/examples/spin/Book_1991/p347.pftp.ses5.pml
- /usr/local/share/examples/spin/Book_1991/p347.pres.sim.h
- /usr/local/share/examples/spin/Book_1991/p347.session.prog.h
- /usr/local/share/examples/spin/Book_1991/p94.pml
- /usr/local/share/examples/spin/Book_1991/p95.1.pml
- /usr/local/share/examples/spin/Book_1991/p95.2.pml
- /usr/local/share/examples/spin/Book_1991/p96.1.pml
- /usr/local/share/examples/spin/Book_1991/p96.2.pml
- /usr/local/share/examples/spin/Book_1991/p97.1.pml
- /usr/local/share/examples/spin/Book_1991/p97.2.pml
- /usr/local/share/examples/spin/Book_1991/p99.pml
- /usr/local/share/examples/spin/Exercises/
- /usr/local/share/examples/spin/Exercises/ex_1a.pml
- /usr/local/share/examples/spin/Exercises/ex_1f.pml
- /usr/local/share/examples/spin/Exercises/ex_2.pml
- /usr/local/share/examples/spin/Exercises/ex_3a.pml
- /usr/local/share/examples/spin/Exercises/ex_3b.pml
- /usr/local/share/examples/spin/Exercises/ex_3c.pml
- /usr/local/share/examples/spin/Exercises/ex_4.pml
- /usr/local/share/examples/spin/Exercises/ex_5.pml
- /usr/local/share/examples/spin/Exercises/ex_6.pml
- /usr/local/share/examples/spin/LTL/
- /usr/local/share/examples/spin/LTL/bakery.pml
- /usr/local/share/examples/spin/LTL/diskhead.pml
- /usr/local/share/examples/spin/LTL/leader.pml
- /usr/local/share/examples/spin/LTL/leader_pre.pml
- /usr/local/share/examples/spin/LTL/ltl_always_eventually.pml
- /usr/local/share/examples/spin/LTL/ltl_example.pml
- /usr/local/share/examples/spin/LTL/ltl_gen.pml
- /usr/local/share/examples/spin/LTL/mobile1.pml
- /usr/local/share/examples/spin/LTL/mobile2.pml
- /usr/local/share/examples/spin/LTL/patterns.pml
- /usr/local/share/examples/spin/LTL/petersonN.pml
- /usr/local/share/examples/spin/LTL/pftp.pml
- /usr/local/share/examples/spin/LTL/salesman1.pml
- /usr/local/share/examples/spin/LTL/salesman2.pml
- /usr/local/share/examples/spin/LTL/train.pml
- /usr/local/share/examples/spin/LTL/zune.pml
- /usr/local/share/examples/spin/README_tests.txt
- /usr/local/share/examples/spin/abp.pml
- /usr/local/share/examples/spin/calculator.pml
- /usr/local/share/examples/spin/cambridge.pml
- /usr/local/share/examples/spin/dtp.pml
- /usr/local/share/examples/spin/eratosthenes.pml
- /usr/local/share/examples/spin/for_example.pml
- /usr/local/share/examples/spin/for_select_example.pml
- /usr/local/share/examples/spin/hajek.pml
- /usr/local/share/examples/spin/hello.pml
- /usr/local/share/examples/spin/leader0.pml
- /usr/local/share/examples/spin/leader_trace.pml
- /usr/local/share/examples/spin/life.pml
- /usr/local/share/examples/spin/loops.pml
- /usr/local/share/examples/spin/manna_pnueli.pml
- /usr/local/share/examples/spin/pathfinder.pml
- /usr/local/share/examples/spin/peterson.pml
- /usr/local/share/examples/spin/priorities.pml
- /usr/local/share/examples/spin/rtos1.pml
- /usr/local/share/examples/spin/sat.pml
- /usr/local/share/examples/spin/snoopy.pml
- /usr/local/share/examples/spin/sort.pml
- /usr/local/share/examples/spin/welfare.pml
- /usr/local/share/examples/spin/werkplaats.pml
- /usr/local/share/examples/spin/wordcount.pml