debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Did some refactoring in the Boogie driver.	wuestholz	2013-06-03
\|
*	Did some refactoring in the Boogie driver.	wuestholz	2013-06-03
\|
*	Did some refactoring in the Boogie driver.	wuestholz	2013-06-03
\|
*	Did some refactoring in the Boogie driver.	wuestholz	2013-06-03
\|
*	Did some refactoring in the Boogie driver.	wuestholz	2013-06-03
\|
*	Fixed an issue with discovering program snapshots.	wuestholz	2013-06-03
\|
*	Added a feature for verifying several program snapshots (incl. result ↵	wuestholz	2013-06-02
\| \| \| \|	caching and prioritization).
*	Changed the prover interface to report traces for time outs and out of memory.	wuestholz	2013-05-30
\|
*	fixed bug in reporting the number of typechecking errors	Unknown	2013-05-22
\| \| \| \|	updated answer file
*	Merge	Unknown	2013-05-18
\|\
* \|	reworked the linear and og implementation based on available variables theory	Unknown	2013-05-18
\| \|
\| *	Adapted Houdini algorithm to take staging into account	allydonaldson	2013-05-18
\|/
*	AbsHoudini: Tolerate some assertion failing. Updated regression baseline.	akashlal	2013-05-10
\|
*	merging changes for fixedpoint engine backend	Ken McMillan	2013-05-07
\|\
* \|	Adding fixedpoint engine backend	Ken McMillan	2013-05-07
\| \|
\| *	AbsHoudini: Each function can specify its own abstract domain. Also added	akashlal	2013-05-05
\| \| \| \| \| \| \| \|	typechecking
\| *	Merge	Unknown	2013-05-04
\| \|\
\| * \|	fixed bug reported by Akash	Unknown	2013-05-04
\|/ /
\| *	Some code refactoring	akashlal	2013-05-03
\|/
*	Merge	allydonaldson	2013-04-30
\|\
* \|	Staged Houdini	allydonaldson	2013-04-30
\| \|
\| *	AbsHoudini: Added support for /errorLimit:n, n > 1	akashlal	2013-04-25
\| \|
\| *	AbsHoudini: Added predicate-abstraction domain and some examples.	akashlal	2013-04-25
\| \|
\| *	AbsHoudini: Added support for DoNotUsLabels, domain for simulating Houdini,	akashlal	2013-04-25
\| \| \| \| \| \| \| \|	few bug fixes, hack to support missing prover declarations.
\| *	AbsHoudini: Added SCC-based worklist, bug-fix for inline attribute,	akashlal	2013-04-19
\| \| \| \| \| \| \| \|	intervals domain
\| *	AbsHoudini: Added support for /inlineDepth, and fixed the regression tests	akashlal	2013-04-18
\| \| \| \| \| \| \| \|	(all pass)
\| *	Nice clean re-implementation of AbstractHoudini. And tests	akashlal	2013-04-18
\|/
*	fixed bugs in both parallel calls and linear stuff (reported by Chris)	Unknown	2013-03-03
\| \| \| \|	also added improved error reporting suggested by Chris
*	fixed bug in OG	Unknown	2013-02-01
\| \| \| \|	added another OG sample illustrating rely-guarantee encoding
*	made a whole bunch of changes to linear and og stuff	Unknown	2013-01-29
\|
*	bug fix reported by Chris	Unknown	2013-01-28
\|
*	added owicki-gries and linear-set to boogiedriver	Unknown	2013-01-25
\| \| \| \|	cleaned up the async type checking
*	Output to Boogie\Binaries even in the Release version	Unknown	2013-01-25
\|
*	Some more changes to AbsHoudini	akashlal	2012-12-28
\|
*	AbstractHoudini: bug fixes	akashlal	2012-12-16
\|
*	More stuff for abstract houdini; updated test case	Unknown	2012-12-10
\|
*	Allow richer spec for abs-houdini	Unknown	2012-12-03
\|
*	Added Abstract Houdini: an implementation of Houdini based on abstract domains.	Unknown	2012-11-05
\| \| \| \|	Currently only predicate-abstraction domain is supported.
*	added sound loop unrolling	Yannick Welsch	2012-07-03
\|
*	bunch of refactorings	Unknown	2012-10-03
\| \| \| \| \| \| \| \| \|	- moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs
*	Removed AIFramework from Boogie -- use native trivial or native ↵	boehmes	2012-09-27
\| \| \| \| \| \| \|	interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped.
*	Removed abandoned Isabelle prover backend	boehmes	2012-09-27
\|
*	Boogie: added /tracePOs option for printing out number of proof obligations ↵	Unknown	2012-09-10
\| \| \| \|	without also printing out the verification times
*	BoogieDriver: correctly display time taken by prover if >60 seconds	Peter Collingbourne	2012-07-30
\|
*	Boogie: formated elapsed time	Jason Koenig	2012-06-28
\|
*	integrating predication	qadeer	2012-06-19
\|
*	testing a fix in SI	qadeer	2012-06-07
\| \| \| \| \|	also changing back the output path in BoogieDriver also disabling z3api for now since it does not build
*	Merging again	Ken McMillan	2012-06-07
\|\
\| *	Trying to merge with recent changes, failing.	Ken McMillan	2012-06-05
\| \|\
\| \| *	Some changes to support expanded use of z3api.	Ken McMillan	2012-06-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Should not affect function of other provers. There is an option added in Check.cs to allow creation of a Checker with a user-specified ProverContext. Also, some extension of z3api prover context to support conversion of Z3 formulas back to VCExpr. Finally, some experimental code, not enabled, to allow conversion of loops to recursion with "head recursion" rather than "tail recursion" (i.e., recursive call before loop body rather than after).