summaryrefslogtreecommitdiff
path: root/Source/Concurrency/MoverCheck.cs
Commit message (Collapse)AuthorAge
* cleaned up some namesGravatar Shaz Qadeer2015-09-28
|
* modified desugaring so that in commutatitivity checks copies of originalGravatar qadeer2015-06-17
| | | | codeexpr is made.
* fixed the treatment of externGravatar qadeer2015-04-17
|
* strengthened type checkingGravatar qadeer2014-12-26
| | | | | cleaned up the generation of mover checks (based on example from Chris) added two examples from Chris to regressions
* some refactoring to separate the concept of shared variables under ↵Gravatar qadeer2014-12-17
| | | | refinement checking with all global variables
* systematic renaming of phase to layerGravatar qadeer2014-12-15
|
* renamed :phase to :layerGravatar qadeer2014-11-14
|
* Did more refactoring and addressed several todos.Gravatar wuestholz2014-09-23
|
* checkpointGravatar qadeer2014-05-03
|
* bug fix in the last updateGravatar qadeer2014-04-25
|
* updated the mover checksGravatar qadeer2014-04-25
|
* added the framing for the refinement checkGravatar qadeer2014-04-16
|
* added variable hidingGravatar qadeer2014-04-16
| | | | added annotation on an atomic action about the phases in which it exists
* added more types to constructed expressionsGravatar qadeer2014-04-15
|
* resolved expressions created during generation of procedures for mover checksGravatar qadeer2014-04-14
|
* fixed a problem with the nonblocking checkGravatar qadeer2014-02-10
|
* added nonblocking checker for left moversGravatar qadeer2014-02-07
|
* new design for linear types + VCgenGravatar qadeer2014-02-07
| | | | | ported all the examples added the QED examples to runtest.bat
* some small optimizations to mover checkingGravatar qadeer2014-01-22
| | | | added LookUp to multiset.bpl
* various bug fixesGravatar qadeer2014-01-21
| | | | added "cnst" feature
* fixed lots of bugs in mover checking codeGravatar qadeer2014-01-14
|
* fixed bug in optimization of commutativity checkGravatar qadeer2014-01-14
|
* added more information to assert messagesGravatar qadeer2014-01-14
|
* Existential failure checker replaced with universal.Gravatar stasiran2014-01-13
|
* extended NormalSubstituter so that it can take in a forold substitutionGravatar qadeer2014-01-10
| | | | optimized the FailurePreservationChecker to eliminate some quantifiers
* implemented a simple quantifier elimination for havoc commands in computing ↵Gravatar qadeer2014-01-09
| | | | | | transition relation changed the type checking of left movers; they are required to be non-blocking now
* some optimizations to mover checksGravatar qadeer2014-01-09
|
* first cut of refinement checkingGravatar qadeer2014-01-07
|
* fixed a bug in mover checking; wasn't generating enough commutativity checksGravatar qadeer2013-12-25
|
* bug fixes in Duplicate.cs and parsing of invariant attributesGravatar qadeer2013-12-22
| | | | other bug fixes in QED stuff
* more refactoring of the concurrency stuffGravatar qadeer2013-12-20
|
* various updates and tighter integration of QED stuff into mainlineGravatar qadeer2013-12-19
|
* added syntax for par call and ParCallCmdGravatar qadeer2013-12-16
|
* some refactoring of QED stuffGravatar qadeer2013-12-10
|
* moved some files aroundGravatar qadeer2013-11-22