summaryrefslogtreecommitdiff
path: root/Source/BoogieDriver/BoogieDriver.cs
Commit message (Expand)AuthorAge
* /contractInfer always prints the computed assignment nowGravatar qadeer2011-11-16
* Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLine...Gravatar Rustan Leino2011-11-15
* added the option /inlineDepth:n. This option defaults to -1. If the user prov...Gravatar qadeer2011-11-13
* moved the addition of selectors and testers to program.ResolveGravatar qadeer2011-11-11
* copied all attributes of the constructor (except for :constructor) to the sel...Gravatar qadeer2011-11-09
* added membership testsGravatar qadeer2011-10-05
* implementing datatypesGravatar qadeer2011-10-05
* updated Houdini so it works with SMTLibGravatar qadeer2011-09-27
* further updates to bit vector analysisGravatar qadeer2011-08-09
* various changes to boogie for bitvector analysis and bctproviderGravatar qadeer2011-08-08
* further changes for making houdini workGravatar qadeer2011-08-04
* cleaned up houdini optionsGravatar qadeer2011-08-04
* Avoid restarting the theorem prover for stratified inlining because itGravatar Unknown2011-06-25
* Boogie: added features to help with modular verification. In particular, defi...Gravatar Rustan Leino2011-05-13
* Stratified inlining: Added concrete values to error traces. Added an extra fl...Gravatar akashlal2011-02-17
* Dafny: removed CEV instrumentationGravatar rustanleino2011-02-03
* Add functions generated in lambda-expansion of function body to top-level pro...Gravatar MichalMoskal2010-12-17
* Refactoring: pulled out all code for stratified inlining to a new file.Gravatar akashlal2010-11-23
* Make the -mv option use the new Model class.Gravatar MichalMoskal2010-10-12
* Get rid of some CCI dependencies in DriverGravatar MichalMoskal2010-10-07
* Boogie:Gravatar rustanleino2010-09-23
* Fixed an off-by-one error. Added "ReachedBound" as a valid boogie outcome.Gravatar akashlal2010-09-18
* Dafny:Gravatar rustanleino2010-09-14
* Fix for extractLoopsGravatar akashlal2010-09-04
* Added a way of recovering counterexample paths after loop extraction. Stable,...Gravatar akashlal2010-09-01
* Boogie: Removed a completed task commentGravatar tabarbe2010-08-19
* Added the option /extractLoops to extract loops as procedure calls. If eithe...Gravatar qadeer2010-08-11
* Boogie: Changed BoogieDriver.cs to use a copy of cce.cs, rather than an inter...Gravatar tabarbe2010-07-30
* <Boogie> <BoogieDriver> Committing my porting of BoogieDriver.cs and the chan...Gravatar tabarbe2010-07-14
* Renaming the old boogiedriver sources in preparation for syncing my ported ch...Gravatar tabarbe2010-07-13
* These 2 files are remnants of attempting the earlier planned method of renami...Gravatar tabarbe2010-07-01
* I am working to port Boogie from Spec# to C#. As part of this process, I nee...Gravatar tabarbe2010-06-30
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-05 19:05:40 +0000