debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
* \|	Some proper naming done in YieldTypeChecker	kuruis	2014-01-12
\| \|
* \|	extended NormalSubstituter so that it can take in a forold substitution	qadeer	2014-01-10
\| \| \| \| \| \| \| \|	optimized the FailurePreservationChecker to eliminate some quantifiers
* \|	implemented a simple quantifier elimination for havoc commands in computing ↵	qadeer	2014-01-09
\| \| \| \| \| \| \| \| \| \| \| \|	transition relation changed the type checking of left movers; they are required to be non-blocking now
* \|	small update to the example	qadeer	2014-01-09
\| \|
* \|	some optimizations to mover checks	qadeer	2014-01-09
\| \|
* \|	a fix regarding the checking of assertions in atomic specs at call sites	qadeer	2014-01-08
\| \|
* \|	Merge	qadeer	2014-01-07
\|\ \
* \| \|	first cut of refinement checking	qadeer	2014-01-07
\| \| \|
\| * \|	added a test to check for stackoverflowexception	akashlal	2014-01-07
\| \| \|
\| * \|	Recursive walking of Exprs doesn't play nice when the depth of the AST is high.	akashlal	2014-01-07
\|/ / \| \| \| \| \| \| \| \|	Reduce depth of AST whenever possible (e.g., use a binary tree instead of a linear list of terms)
* \|	points on "home strecth of yield type checker" added	kuruis	2014-01-04
\| \|
* \|	Updated year in main copyright message	Rustan Leino	2014-01-03
\| \|
* \|	and another	qadeer	2014-01-03
\| \|
* \|	another small fix	qadeer	2014-01-03
\| \|
* \|	some fixes	qadeer	2014-01-03
\| \|
* \|	First rough draft of refinement checking.	stasiran	2014-01-03
\| \|
* \|	First rough draft of refinement checking.	stasiran	2014-01-03
\| \|
* \|	minor bug in traversing program fixed	kuruis	2014-01-03
\| \|
* \|	some bugs related with phases fixed	kuruis	2014-01-03
\| \|
* \|	another fix	qadeer	2014-01-02
\| \|
* \|	some more fixes to examples	qadeer	2014-01-02
\| \|
* \|	Merge	qadeer	2014-01-02
\|\ \
* \| \|	more fixes	qadeer	2014-01-02
\| \| \|
\| * \|	debug pragma closed	kuruis	2014-01-02
\| \| \|
* \| \|	Merge	qadeer	2014-01-02
\|\\| \|
* \| \|	some more fixes	qadeer	2014-01-02
\| \| \|
\| * \|	some fixes on devicedriver example	kuruis	2014-01-02
\|/ /
* \|	Error reporting with line numbers and commands of trace is provided	kuruis	2014-01-02
\| \|
* \|	some proper yield check reporting provided	kuruis	2014-01-02
\| \|
* \|	fixed examples to deal with yield type checking errors	qadeer	2014-01-01
\| \|
* \|	some bugs fixed on yiledtypechecker	kuruis	2013-12-31
\| \|
* \|	made some fixes to type checking of atomic actions	qadeer	2013-12-31
\| \|
* \|	made some fixes	qadeer	2013-12-29
\| \|
* \|	Some bugs in yieldtypesafe fixed	kuruis	2013-12-29
\| \|
* \|	yieldtypesafe and yieldreachability automatons are separated.	kuruis	2013-12-29
\| \| \| \| \| \| \| \| \| \|	integration of parallel call cmds done points (1 and 3) on Shaz's email are done
* \|	fixed vc generation so that even when builtin array functions are used,	qadeer	2013-12-28
\| \| \| \| \| \| \| \|	the program can be verified without the use of /useArrayTheory
* \|	Fixed a bug regarding the treatment of old() in stable procedures. The ↵	qadeer	2013-12-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	implementation of the stable procedure interprets old() as the state at the beginning of the procedure's execution but the caller of the procedure interprets old() as the state just before the call. The fix bridges the mismatch between these two interpretations.
* \|	fixed a bug in mover checking; wasn't generating enough commutativity checks	qadeer	2013-12-25
\| \|
* \|	Merge	qadeer	2013-12-24
\|\ \
* \| \|	more bug fixes	qadeer	2013-12-24
\| \| \| \| \| \| \| \| \| \| \| \|	updates to DeviceCache.bpl to make it verify
\| * \|	Regex fixed after discussion with Shaz	kuruis	2013-12-24
\| \| \|
* \| \|	Merge	qadeer	2013-12-23
\|\\| \|
* \| \|	updates	qadeer	2013-12-23
\| \| \|
\| * \|	Automata debugging done on YieldTypeChecker.	kuruis	2013-12-23
\|/ / \| \| \| \| \| \|	Regex must be revisited
* \|	more bug fixes	qadeer	2013-12-22
\| \|
* \|	bug fixes in Duplicate.cs and parsing of invariant attributes	qadeer	2013-12-22
\| \| \| \| \| \| \| \|	other bug fixes in QED stuff
* \|	strengthened type checking w.r.t. qed vs non-qed global variables	qadeer	2013-12-21
\| \|
* \|	more refactoring of the concurrency stuff	qadeer	2013-12-20
\| \|
* \|	comparison of phase_num checks updated	kuruis	2013-12-20
\| \|
* \|	Minor Changes in YieldTypeChecker	kuruis	2013-12-19
\| \|