debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	some small optimizations to mover checking	qadeer	2014-01-22
\| \| \| \|	added LookUp to multiset.bpl
*	various bug fixes	qadeer	2014-01-21
\| \| \| \|	added "cnst" feature
*	bug fix: if an absy is not reachable, make the set of available vars empty at it	qadeer	2014-01-21
\|
*	bug fix in handling of parallel call	qadeer	2014-01-20
\|
*	Added functionality to rename state captures when programs are unrolled.	Ally Donaldson	2014-01-17
\|
*	Merge	Ally Donaldson	2014-01-17
\|\
* \|	Integrated support for k-induction, implemented a while ago by Philipp ↵	Ally Donaldson	2014-01-17
\| \| \| \| \| \| \| \|	Ruemmer but never previously committed.
\| *	bug fix in error trace printing	qadeer	2014-01-16
\| \|
\| *	fix for a completeness bug (reported by Serdar) in refinement checker	qadeer	2014-01-16
\| \|
\| *	Clean up of yield type checker	qadeer	2014-01-16
\| \|
\| *	in the middle of cleaning up yield type checker	qadeer	2014-01-15
\| \|
\| *	fixed lots of bugs in mover checking code	qadeer	2014-01-14
\| \|
\| *	fixed bug in optimization of commutativity check	qadeer	2014-01-14
\| \|
\| *	Merge	qadeer	2014-01-14
\| \|\ \| \|/ \|/\|
\| *	added more information to assert messages	qadeer	2014-01-14
\| \|
* \|	Fix Boogie so it compiled with mono. Patch by Dan Liew.	Ally Donaldson	2014-01-14
\|/
*	Existential failure checker replaced with universal.	stasiran	2014-01-13
\|
*	a bug fix	qadeer	2014-01-13
\|
*	eliminated use of assertionPhaseNums	qadeer	2014-01-13
\|
*	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
*	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
\| \|
\| *	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
\|
*	debug pragma closed	kuruis	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
\|
*	some bugs fixed on yiledtypechecker	kuruis	2013-12-31
\|
*	made some fixes to type checking of atomic actions	qadeer	2013-12-31
\|
*	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
\|/