Skip to content
Snippets Groups Projects
Select Git revision
  • array-assignment-wlp
  • bw-wip/program-path-generation
  • master default protected
  • parser-extension
  • wlp-determination
5 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.010Nov129Oct2823181614131228Sep27242120181715Improve READMEmastermasterAdd a READMEAdd Atom counterAdd branch checking heuristicFixed benchmarking process and added output generationImplemented benchmarking functionalityAdd TreeTrimmingMode and CLI parameter thereofAdded timing functions for z3 verification and tree trimmingFixed bugs in the tree trimmer and it uses the experimentation parameter. Removed unused time checks in VerfifierImprove output, use tree trimmer 2000Finish ProgramPathTreeAdd version constraint to shellyImplemented the tree trimmer 2000. Can trim trees faster than you can say pony on a pickle.Add ProgramPathTreeAdd better outputMerge branch 'master' of https://git.science.uu.nl/b.wijgers/psv-practicalAdd parser librarZ3Runner no longer crashes the verifier upon exception and added NOT expr before wlp to z3 conversionFixed benchmarksAdd experiment parameter and benchmark programsImplemented sizeOf array in z3Merge branch 'added-timing-and-z3-fix' into 'master'Extended Z3 Theorem to support arrays and fixed a bug in forall expressionAdded time calculation to verifierAdd function to find all variable decls in programMerge branch 'simplify-expressions' into 'master'Simplify more expressionsMerge branch 'add-options' into 'master'Added config options and improved main output formatMerge branch 'implemente-z3' into 'master'implemented-z3-theorem-and-runnerAdd forall for logical expressionsRemove debug tracing from WLP calculationarray-assignmen…array-assignment-wlpAdd AAssign WLP calculationAdd scanSumExampleSimplify LogicalExpressions by extracting ExprsAdd calculation for WLPs from ProgramPathswlp-determinationwlp-determinationAdd "normalizeProgramPath" to WLP.ProgramPathRemove superfluous "skip"s from abs exampleUpdate the parser