debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
\| *	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
\| \|
\| *	Minor changes to AbstractHoudini	akashlal	2013-03-10
\|/
*	Refactored MatchCandidate	allydonaldson	2013-03-08
\|
*	MatchCandidate modified to match candidates by variable name, rather than by ↵	allydonaldson	2013-03-08
\| \| \| \|	variable identity. ApplyAssignment method added, which takes a program (not necessarily the same program on which Houdini was invoked, but a program that has the same candidate set), and applies the Houdini assignment to the program.
*	AbstractHoudini: more details for computing a tighter predicate cover	Unknown	2013-02-15
\|
*	Timeout in AbstractHoudini	akashlal	2013-01-16
\|
*	Some code clean-up	Unknown	2013-01-07
\|
*	Some more changes to AbsHoudini	akashlal	2012-12-28
\|
*	minor bug fix	Unknown	2012-12-27
\|
*	AbstractHoudini optimization: replace summary predicate with Boolean variables	Unknown	2012-12-21
\| \| \| \|	(just like stratified inlining)
*	Bug fix for ExplainHoudini. Made it robust under timeouts.	Unknown	2012-12-20
\|
*	AbstractHoudini: more fixes, for self-recursion	akashlal	2012-12-16
\| \| \| \|	and Bilateral at the same time.
*	AbstractHoudini: bug fixes	akashlal	2012-12-16
\|
*	AbstractHoudini: support for generating a witness	Unknown	2012-12-15
\|
*	Added some comments	akashlal	2012-12-12
\|
*	Merge	akashlal	2012-12-12
\|\
* \|	First implementation of ExplainHoudini	Unknown	2012-12-12
\| \|
\| *	Houdini: allow cross-dependencies between procedures that occurs when assume	Unknown	2012-12-11
\| \| \| \| \| \| \| \|	and assert commands in implementations have existential constants
* \|	More stuff for abstract houdini; updated test case	Unknown	2012-12-10
\|/
*	Bug fix for abstract-houdini	Unknown	2012-12-07
\|
*	Allow richer spec for abs-houdini	Unknown	2012-12-03
\|
*	when a query times out, all asserted candidates are dropped	Unknown	2012-11-25
\|
*	Minor refactorings for integrating corral	Unknown	2012-11-18
\|
*	Added Abstract Houdini: an implementation of Houdini based on abstract domains.	Unknown	2012-11-05
\| \| \| \|	Currently only predicate-abstraction domain is supported.
*	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.
*	Extra debugging output for Houdini	Unknown	2012-08-21
\|
*	Houdini: recognise candidates of the form (p => (q => (... => (e => phi)))) ↵	Peter Collingbourne	2012-08-07
\| \| \| \|	where e existential
*	moved class Macro to Absy	qadeer	2012-06-04
\| \| \| \| \|	cleanup up DefineMacro Changed SI to use macros for reach info
*	changed behavior of InlinedEnsures so that free ensures is skipped unless an ↵	qadeer	2012-06-01
\| \| \| \|	attribute called :assume is there
*	starting the implementation of the new stratified inlining API	qadeer	2012-05-21
\|
*	shutting down the prover used for doing houdini	qadeer	2012-05-10
\|
*	clean up in stratified inlining	qadeer	2012-04-29
\|
*	removed lazy inlining	qadeer	2012-04-28
\|
*	unsat core for houdini	qadeer	2012-04-27
\|
*	various changes for using unsat cores in Houdini	qadeer	2012-04-17
\|
*	houdini cleanup continued	qadeer	2012-03-10
\|
*	various refactorings related to houdini	qadeer	2012-03-02
\|
*	various cleanup regarding /doNotUseLabels	qadeer	2012-02-28
\|
*	further fixes related to using uninterpreted function for error traces	qadeer	2012-02-25
\| \| \| \|	removed Provers.Simplify, Provers.Z3, Provers.TPTP from the solution
*	bug fixes related to using ControlFlowFunction instead of labels	qadeer	2012-02-23
\|
*	slight change to houdini logging	Unknown	2012-02-06
\|
*	added more logging in houdini	Unknown	2012-02-06
\|
*	Use DateTime.UtcNow instead of DateTime.Now	stobies	2012-01-11
\| \| \| \|	see http://blogs.msdn.com/b/kirillosenkov/archive/2012/01/10/datetime-utcnow-is-generally-preferable-to-datetime-now.aspx
*	bug fix in the FreeRequiresVisitor	qadeer	2011-12-22
\|
*	removed some extraneous parameters	qadeer	2011-12-19
\|
*	fixed a completeness problem in houdini with inlining	qadeer	2011-12-18
\|