A forum for Spin users
You are not logged in.
Interesting -- what error message do you get with Tcl/Tk >= 9?
at https://codescrub.com/ you will now find a PDF of an updated version of the Cobra book.
easier to get, more up to date, and a comprehensive overview of the fastest static code analyzer available today.
It is available on amazon:
https://www.amazon.com/dp/B0FFVZC8F1?ref_=pe_93986420_774957520
for more information (table of contents etc) see:
https://codescrub.com
that is true -- to account of out of order memory access you'd need to extend the model
an example of what it takes to do this is:
https://spinroot.com/spin/Doc/course/x86_tso.pml
a new user guide for the Cobra tool is available as PDF,
with detailed descriptions of Cobra's options and examples.
you can volunteer to be a reviewer for the final draft (december 2024)
The next Caltech course CS118 will be held Jan-Mar 2025, but you can take pretty much the same material in the online course available through the spinroot webpage
https://spin-web.github.io/SPIN2025
The 31st International Symposium on Model Checking Software will be held May 7-8 2025 in Hamilton, Canada, co-located with ETAPS-2025. The Symposium is organized by Kristin Yvonne Rozier and Gidon Ernst.
Available on github (nimble-code) or https://spinroot.com/cobra
A significant extension of Cobra's capabilities, with many new predefined query libraries, options for statistical analysis of code and finding code duplicates and cloned code segments.
A new user manual is currently in review -- if you'd like to help review the draft, send a message.
The latest release of the interactive static source code analyzer Cobra is now available on Githib.
Much new functionality and improvements. Give it a try.
The next Spin Symposium will be held April 26-27, 2023, co-located with ETAPS 2023.
For more information:
https://easychair.org/cfp/SPIN-2023
or
https://spin-web.github.io/SPIN2023/
The current version of the Cobra static analyzer is now on Github, and includes a new GUI, iCobra.
Many new query libraries and expanded capabilities to work with search pattern sets.
The Caltech course CS118 is offered again this winter-term (Jan-Mar 2023).
The 28th International Spin Symposium will be held May 21-22, 2022, in Chicago Illinois, organized by Owolabi Legunsen and Grigore Rosu.
Papers were due: March 25, 2022
Author notifications: April 29, 2022
Camera ready papers: May 9, 2022
good point
the .(goto) links are generated by the parser. e.g. to encode break statements etc
correct -- the d_step sequences are converted into a single transition.
you can see the automata structure that is used with: $ ./pan -d
they should be basic statements from the model
so it's mostly Promela syntax -- d_steps are special though
since they are converted into a single transition
a channel name is a variable that can hold the id of an instantiated channel
the same channel name could, for instance, be reassigned the id of different channels
at different points in a run
for a given instantiated channel, the id number does not change, but a channel variable
can hold any channel id at different points in it's use
where are they marked as sub-sequences?
can you give an example?
proctypes and never claims are converted into omega-automata, which have numbered states...
not sure what you mean by "the sublanguage that can occur in traces"
you mean the format and syntax of error traces?
yes, you can run the preprocessor manually (call gcc -E -x c model.pml)
just like spin does internally (main.c line 106)
it has to do with the implementation of partial order reduction
where we want to make it impossible to negate expressions
that can be used to optimize the verification
the output of the -I flag is not a valid Promela model -- it's mostly a debugging aid to see how inlines and macros are expanded internally