v6.27.14

Various XSTS, MDD and witness fixes, optimizations

Modified subprojects (since v6.27.9):
common/analysis
common/common
xsts/xsts
xsts/xsts-cli

v6.27.9

Witness fix (rejecting 2.0 for violation concurrency)

Modified subprojects (since v6.27.4):
common/analysis
xcfa/xcfa-analysis
xcfa/xcfa-cli
xsts/xsts-analysis
xsts/xsts-cli

SV-COMP'26 final submission

This release contains binaries for the SV-COMP'26 competition.

The 3 binary artifacts in this release are:

• Theta - our best selection of proven algorithms,
• EmergenTheta - the up-and-coming (emergent) technologies we want to try but haven't thoroughly tested, and
• Thorn - our light-weight verification configuration which delegates to external CHC solvers for model checking.

Minimal necessary packages for Ubuntu 24.04 LTS:

• openjdk-17-jre-headless or newer versions
• libgomp1
• libmpfr-dev

What's Changed

• LTL checking by @RipplB in #311
• ECBS modifications by @mondokm in #336
• Added monolthic l2s conversion by @mondokz in #337
• Added IC3 by @dantpu in #339
• IC3 by @mondokm in #340
• IC3 bugfix by @mondokm in #344
• aiger hotfix by @leventeBajczi in #343
• added smthome to sts-cli by @leventeBajczi in #346
• Petri-net properties implemented: safe, deadlock by @leventeBajczi in #349
• Update MddChecker to use MonolithicExpr by @mondokm in #345
• Fix MonolithicExprs missing params and Reverse by @leventeBajczi in #350
• Fix abstract by @leventeBajczi in #351
• AIGER format update by @leventeBajczi in #347
• (x)sts fix by @leventeBajczi in #353
• OC checker improvements by @csanadtelbisz in #354
• Fix horn solving for termination by @leventeBajczi in #342
• Fix tests by @leventeBajczi in #359
• Fix rounding by @leventeBajczi in #357
• Fixed bug related to enum type inference in XSTS by @mondokm in #360
• MDD performance improvements by @mondokm in #363
• Handle RatExprs in MDDs by @mondokm in #364
• On-the-fly reachability checking for MDDs by @mondokm in #367
• Added initial havoc by @leventeBajczi in #365
• Added zenodo uploading to chain of releases by @leventeBajczi in #370
• Zenodo release secret fix by @leventeBajczi in #371
• Typo in zenodo release by @leventeBajczi in #372
• Update metadata.json for zenodo by @leventeBajczi in #373
• Added model generation to CHC frontend (WiP) by @leventeBajczi in #369
• Update metadata.json by @leventeBajczi in #374
• MDD counterexample generation and implicit CEGAR by @mondokm in #377
• XCFA MDD Trace by @mondokm in #379
• Identity detection, MonolithicExpr splitting by @mondokm in #381
• XSTS MDD improvements by @mondokm in #380
• Chccomp final update by @leventeBajczi in #382
• PNML parsing fix by @mondokm in #383
• Timeout for MDD trace generation and BV simplify fix by @mondokm in #385
• Fix issue with variable equalities in if and nondet stmts by @mondokm in #386
• Monolithic expression pass pipeline by @RipplB in #388
• XSTS MDD fixes by @mondokm in #387
• Fix issue with simple saturation and improve identity detection by @mondokm in #389
• Var ordering improvements by @mondokm in #392
• Xcfa multithread to monolithic by @csanadtelbisz in #404
• Xcfa multithread to monolithic by @csanadtelbisz in #405
• Xcfa multithread to monolithic by @csanadtelbisz in #406
• Xcfa multithread to monolithic by @csanadtelbisz in #407
• Transver update by @leventeBajczi in #403
• Various XCFA improvements by @csanadtelbisz in #391
• Update SMT-LIB solvers to their most recent versions by @as3810t in #411
• #408 Refactored the Gradle build step from the Docker image build process by @arminzavada in #409
• Struct patch by @leventeBajczi in #378
• Fixed location mapping by @leventeBajczi in #384
• Javasmt update by @leventeBajczi in #375
• EXPL_PRED_STMT and EXPL_PRED_SPLIT domain for XCFA by @mondokm in #396
• Fix label c by @leventeBajczi in #418
• Output options refactor by @csanadtelbisz in #420
• Trace generation by @AdamZsofi in #401
• No overflow by @leventeBajczi in #421
• Coverage calculation update by @leventeBajczi in #424
• Fixing the frontend failures hopefully by @leventeBajczi in #425
• Xcfa multithread to monolithic by @csanadtelbisz in #412
• Fixing several reachability witness issues by @AdamZsofi in #426
• Frontend fix for witness by @leventeBajczi in #428
• Zenodo update by @leventeBajczi in #435
• Deref to array fix by @leventeBajczi in #436
• Fixed pass, bumped version by @leventeBajczi in #438
• Fixed struct initialization by @leventeBajczi in #440
• Fixing initializer lists & memsafety pass by @csanadtelbisz in #444
• Function call location fix by @AdamZsofi in #443
• Svcomp26 various fixes by @leventeBajczi in #448
• Dereferences to array, MDD 2D array, Multithread to monolithic fixes by @mondokm in #439
• Patch trace generation in xsts-cli by @AdamZsofi in #450
• Various fixes around witnesses by @AdamZsofi in #453
• Logging in porfolio nodes changed to use a logger instead of println by @szdan97 in #454
• Some more small xsts tracegen fixes by @AdamZsofi in #456
• MDD optimizations by @mondokm in #390
• OC trace fix by @csanadtelbisz in #458
• Concurrency violation witness fix by @leventeBajczi in #465

New Contributors

• @mondokz made their first contribution in #337
• @dantpu made their first contribution in #339

Full Changelog: svcomp25...svcomp26

v6.27.4

Logging revision

Modified subprojects (since v6.27.3):
cfa/cfa-cli
common/analysis
common/common
xcfa/c2xcfa
xcfa/xcfa-analysis
xcfa/xcfa-cli

v6.27.3

Fixed some witness-related problems

Modified subprojects (since v6.27.1):
xcfa/xcfa
xcfa/xcfa-cli
xsts/xsts-cli

v6.27.1

fix witness

Modified subprojects (since v6.27.0):
xcfa/xcfa
xcfa/xcfa-cli

v6.27.0

Fixed various frontend and portfolio-related stuff for svcomp26

Modified subprojects (since v6.26.5):
common/analysis
common/core
frontends/c-frontend
solver/solver-smtlib
solver/solver-z3
solver/solver-z3-legacy
xcfa/c2xcfa
xcfa/xcfa
xcfa/xcfa-analysis
xcfa/xcfa-cli
xcfa/xcfa2chc

v6.26.5

Fixed struct handling in memory safety category

Modified subprojects (since v6.26.4):
frontends/c-frontend
xcfa/c2xcfa
xcfa/xcfa
xcfa/xcfa-cli

v6.26.4

Minor issue fix in deref to array pass

Modified subprojects (since v6.26.2):
common/common
xcfa/xcfa

v6.26.2

Metadata update for Zenodo

Modified subprojects (since v6.26.1):