Skip to content

v0.1.21

Pre-release
Pre-release
Compare
Choose a tag to compare
@danieldietsch danieldietsch released this 06 Oct 15:25
· 13509 commits to dev since this release
v0.1.21
2977d7c

Features

  • new equality domain (VPDomain) that uses weak equivalences and congruence closures (see #159, #224, #162)
  • InvariantSynthesis now supports algorithm that guesses danger invariants
  • support for reading Floyd-Hoare automata from files
  • preliminary support for reuse of Floyd-Hoare automata (regression verification)
  • now using cell precision for arrays in fault localization
  • new auotmaton operation Relabel: Relabel replaces the labels of all states with numbers. If several operations are executed in a row the names of the states can become very long (and cause OOMs). This operation will give you shorter strings.
  • options for output of statistics as .csv file during normal runs (closes #190)
  • preliminary version of random tree automata generator
  • Ultimate version now also contains the git hash and a modifier if the repository is dirty; the version is printed in CLI and GUI frontends
  • IRD quantifier elimination now uses anti-DER rule

NCSB complementation of (non-deterministic) Büchi automata:

  • integrated new NCSB implementations
  • add support for LazyS optimization to NCSB implementation
  • use new NCSB algorithms in RefineBuchi
  • LazyS optimization for original BuchiComplementNCSB operation
  • BuchiDifference for simple and lazy NCSB

Bugfixes

  • various bugfixes for TreeAutomizer (see #210, #143)
  • fixed bug that lead to a crash when interpreting an .ats file with a TreeAutomaton that contained unused symbols in its alphabet
  • fixed a bug in CrossProducts.binarySelective(...)
  • fixed a bug in ThreeValuedEquivalenceRelation (see #234)
  • various fixes to ElimStorePlain
  • fix nontermination by not computing differences if abstraction is already empty
  • fix bug in AffineTerm: omit zero in RHS if you bring variable to RHS
  • fix bug in fixpoint check for lassos with auxvars (closes #220)
  • various bugfixes and improvements to different loop acceleration modes
  • fix script dumping for SpaceExParser
  • fixed a bug during prelog generation by explicitly specifying the classloader to prevent failures under different classloaders (e.g., during maven or inside tomcat)
  • fixed NPE in backtranslation (if there is no C function, use the boogie name instead of crashing) (closes #215)
  • fixed a bug in nonrelational domains of abstract interpretation where renameVariables() did not rename variables.

Plumbing

Utilities

  • optimization of UnionFind.union(...) -- should run in amortized logarithmic time
  • updated ThreeValuedEquivalenceRelation s.t. it can detect contradictions now
  • reworked CongruenceClosure implementation
  • UnionFind now takes a comparator as parameter and ensures that representatives are always minimal elements in their equivalence class with respect to the given comparator
  • add auxiliary method that computes the "guarded havoc"
  • merged utility classes SetOperations and DataStructureUtils, using the intersection implementation of DataStructureUtils (~20% faster)

Conventions and naming

  • constants of auxVars get the c_aux_ prefix
  • renamed UltimateCore to de.uni_freiburg.informatik.ultimate.core
  • renamed TraceChecker to TraceCheck (closes #229)

SMT and "Ultimate normal form"

  • now using Rational instead of BigInteger and BigDecimal in many places (should be the default way of representing constants)
  • now using negated equality instead of "distinct" in Term
  • added various checks that new terms are in Ultimate normal form
  • now using SmtUtils instead of Util in all places
  • new methods for simplification of and/or
  • `´SmtUtils`` now has a flag that controls extended location simplifications (combating useless simplifications)
  • new feature for SimplifyDDA: Allow to simplify a term with respect to a given context.
  • add method that can transform SMT-Terms given as strings into our Term data structure (very useful for unit tests)
  • extend util function for equalities by a simplification that eliminates self-updates of arrays

CEGAR and refinement engine

  • refactored CEGAR loop
  • use refinement engine for the non-Büchi refinements in termination analysis
  • refinement strategies can now specify their own interpolant acceptance threshold (closes #226)

Abstract interpretation

  • removed IBoogieVar, add getSort() to IProgramVarOrConst, removed VARDECL from abstract interpretation (closes #222)
  • add renameVariable to IAbstractState and implement it for most domains except SMTTheory and VpDomain
  • add IAbstractState.evaluate(...) and pretty inefficient default implementation
  • add methods to IAbstractDomain that will be called before and after fixpoint computation
  • more precise calculations in nonrelational domains of abstract interpretation

Misc

  • CACSL2BoogieTranslatorObserver now tolerates other models
  • TimeoutResults now display long descriptions
  • add BoogieModSetAnnotator to test dependencies
  • move CDTDecorator to CDTParser (required for multiparse, see #37, #38)
  • add option that hides backtranslation warnings in BoogiePreprocessor
  • change build properties s.t. all projects use workspace build properties
  • add new library as dependency of Library-Automata: trove 3.0.3
  • updated SMTInterpol to 2.1-397-g31e711a0

Known Issues

  • README and Website usage instructions outdated (see #135)
  • Startup with generated binary ./Ultimate stalls if no X display is available
  • The SMTInterpol version used in this release contains some unsoundness bugs
Assets 5
Loading