debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Added /printFixedPoint option	Ken McMillan	2014-04-14
\|
*	Added option to avoid unrolling irreducible loops	akashlal	2014-04-06
\|
*	Added /trustNonInterference option	qadeer	2014-02-28
\|
*	added /doNotUseParallelism option	qadeer	2014-02-27
\|
*	Added /trustPhasesDownto option	qadeer	2014-02-24
\|
*	Added /trustPhasesUpto option	qadeer	2014-02-23
\|
*	Added /trustAtomicityTypes option	qadeer	2014-02-22
\|
*	Option for reversing Houdini worklist (for top-down analysis)	akashlal	2014-01-28
\|
*	Integrated support for k-induction, implemented a while ago by Philipp ↵	Ally Donaldson	2014-01-17
\| \| \| \|	Ruemmer but never previously committed.
*	Updated year in main copyright message	Rustan Leino	2014-01-03
\|
*	removed bitvector analysis from Boogie	qadeer	2013-12-08
\| \| \| \|	an advanced version has been moved to Corral
*	code cleanup	akashlal	2013-11-02
\|
*	small refactoring	Pantazis Deligiannis	2013-10-02
\|
*	support for disabling loop entry invariant assertion checking	Pantazis Deligiannis	2013-10-01
\|
*	changes to support a configured errorLimit	Pantazis Deligiannis	2013-09-30
\|
*	more changes towards parallelisation of Houdini	Pantazis Deligiannis	2013-09-29
\|
*	refuted candidates are exchanged in memory using a concurrent dictionary ↵	Pantazis Deligiannis	2013-09-26
\| \| \| \|	instead of using an IO csv file as before
*	new option for reversing the topological order - this could potentially help ↵	Pantazis Deligiannis	2013-08-19
\| \| \| \|	to speedup houdini refutation of candidates
*	new option to disable checking for loop maintained invariants - this leads ↵	Pantazis Deligiannis	2013-08-15
\| \| \| \|	to an underapproximation that helps to speedup houdini refutation of candidates
*	parallel houdini prototype working	Pantazis Deligiannis	2013-07-26
\|
*	Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in ↵	wuestholz	2013-07-22
\| \| \| \|	code (as opposed to contracts).
*	Whitespace fix	Ally Donaldson	2013-07-22
\|
*	Whitespace fix	Ally Donaldson	2013-07-22
\|
*	merge	Pantazis Deligiannis	2013-07-19
\|\
* \|	refactoring and fixes in the SMTLIB2 parser	Pantazis Deligiannis	2013-07-19
\| \|
\| *	Revamp of staged Houdini, and completion of parallel support.	allydonaldson	2013-07-18
\| \|
\| *	Merge	allydonaldson	2013-07-16
\| \|\
\| * \|	Reworking of Staged Houdini in preparation for parallelising it.	allydonaldson	2013-07-16
\| \| \|
* \| \|	Merge	Pantazis Deligiannis	2013-07-15
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	Added an attribute to set the time limit for implementations.	wuestholz	2013-07-12
\| \|/ \|/\|
\| *	merge	Pantazis Deligiannis	2013-07-06
\| \|\
* \| \|	Added an option to verify each input file separately.	wuestholz	2013-07-05
\| \|/ \|/\|
* \|	Added support in the abstract interpreter for an attribute {:identity}, ↵	Rustan Leino	2013-07-05
\| \| \| \| \| \| \| \|	which says that a function is an identity function.
* \|	Merge	allydonaldson	2013-06-18
\|\ \
\| * \|	Added /help and /attrHelp output for program snapshot verification.	wuestholz	2013-06-12
\| \| \|
\| \| *	cvc4 command line option & cvc4.cs in Provers	pantazis	2013-06-12
\| \|/
* \|	Merge	allydonaldson	2013-06-07
\|\\|
* \|	Some work on staged Houdini	allydonaldson	2013-06-07
\| \|
\| *	Added a feature for verifying several program snapshots (incl. result ↵	wuestholz	2013-06-02
\| \| \| \| \| \| \| \|	caching and prioritization).
\| *	Merge changes to support Corral in fixedpoint backend	Ken McMillan	2013-05-29
\|/\|
\| *	Getting fixed point backend to work with Corral.	Ken McMillan	2013-05-29
\| \|
* \|	Improvements to Staged Houdini	allydonaldson	2013-05-29
\| \|
* \|	Staged Houdini can now take a path to a file of ignored variables	allydonaldson	2013-05-27
\|/
*	Adding fixedpoint engine backend	Ken McMillan	2013-05-07
\|
*	Staged Houdini	allydonaldson	2013-04-30
\|
*	made a whole bunch of changes to linear and og stuff	Unknown	2013-01-29
\|
*	Let Boogie clients determine their own version string	Rustan Leino	2013-01-23
\|
*	Use the new ProverInterface's Evaluate method in stratified inlinig	Unknown	2013-01-03
\| \| \| \|	(guarded by the flag /useProverEvaluate)
*	Missed checking this in.	akashlal	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