summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/VC.cs
Commit message (Expand)AuthorAge
* Improve support for optimization and identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-03
* Add simplified may-unverified analysis and instrumentation.Gravatar Valentin Wüstholz2015-11-20
* Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
* Add support for annotating implementations with k-ind. depth.Gravatar Valentin Wüstholz2015-10-29
* Improve output for diagnosing timeouts.Gravatar Valentin Wüstholz2015-09-30
* updateGravatar Shaz Qadeer2015-09-28
* Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2015-08-28
|\
* | Added /verifySnapshots:3, which prints recycled errors messages with the sour...Gravatar Rustan Leino2015-08-28
| * Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
|/
* Add some experimental support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-18
* Fixed minor issue.Gravatar wuestholz2015-01-26
* Minor changeGravatar wuestholz2015-01-26
* Fixed a postcondition.Gravatar wuestholz2014-12-26
* Added an annotation, :split_here, for predicate statements.Gravatar Bryan Parno2014-12-16
* Fixed issue in the verification result caching.Gravatar wuestholz2014-11-10
* Worked on the verification result caching.Gravatar wuestholz2014-10-17
* fixed StackOverflow in TraceCounterexample;Gravatar qadeer2014-09-30
* Did more refactoring and addressed several todos.Gravatar wuestholz2014-09-23
* Did some refactoring.Gravatar wuestholz2014-09-23
* fixed codexpr bug reported by Michael Emmi; removed special handling of codex...Gravatar qadeer2014-08-08
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-07-15
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-10
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-09
* Worked on adding support for "canned errors".Gravatar wuestholz2014-07-07
* Added more tests and worked on adding support for "canned errors".Gravatar wuestholz2014-07-06
* Worked on adding support for "canned errors".Gravatar wuestholz2014-07-06
* Did some refactoring, fixed minor issues, and made it apply the more advanced...Gravatar wuestholz2014-07-06
* OnModel now carries the result of the prover callGravatar akashlal2014-06-28
* Added mechanism for getting the variables referenced by a loop (not just the ...Gravatar Ally Donaldson2014-06-09
* Made VarsAssignedInLoop public, since it can be useful in computing modifies ...Gravatar Ally Donaldson2014-06-06
* Add support for assumption variables.Gravatar wuestholz2014-04-21
* Changed all lambda-expression rewriting to be done as a pre-processing step b...Gravatar Rustan Leino2014-02-28
* Fixed errors in the use of Code ContractsGravatar Rustan Leino2014-02-10
* Added functionality to rename state captures when programs are unrolled.Gravatar Ally Donaldson2014-01-17
* Integrated support for k-induction, implemented a while ago by Philipp Ruemme...Gravatar Ally Donaldson2014-01-17
* Resolve a concurrency issue (reported by Alex Summers).Gravatar wuestholz2013-12-12
* Patch by Nathan Chong: iterative version of remove empty blocks algorithm. T...Gravatar Ally Donaldson2013-12-02
* MergeGravatar Pantazis Deligiannis2013-10-09
|\
* | small refactoringGravatar Pantazis Deligiannis2013-10-02
* | support for disabling loop entry invariant assertion checkingGravatar Pantazis Deligiannis2013-10-01
* | changes to support a configured errorLimitGravatar Pantazis Deligiannis2013-09-30
* | more changes towards parallelisation of HoudiniGravatar Pantazis Deligiannis2013-09-29
| * refactored StratifiedInline.GenerateVC to use GenerateVCAux instead of Genera...Gravatar qadeer2013-09-09
| * fixed bug introduced by the last checkin in letvciterativeGravatar qadeer2013-09-08
| * fixed the problem with codexprsGravatar qadeer2013-09-07
| * When a codeexpr is used at the top-level in an assume statement, we use the a...Gravatar qadeer2013-09-04
| * Factored out the closure for codeexpr conversion so that it can be reused.Gravatar qadeer2013-09-04
| * Applied Chris Hawblitzel's changes to deal with {:expand}Gravatar qadeer2013-08-23
* | MergeGravatar Pantazis Deligiannis2013-08-20
|\|
* | new option to disable checking for loop maintained invariants - this leads to...Gravatar Pantazis Deligiannis2013-08-15