Owner

ftsrg

6 indexed repositories · View on GitHub

theta
Generic, modular and configurable formal verification framework supporting various formalisms and algorithms

Java · 66 stars
semantifyr
A framework to support the declarative definition of engineering model semantics

Kotlin · 5 stars
templates
Public appearance guidelines and logos

TeX · 4 stars
ftsrg.github.io
🔴⚫⭕ New, modern website of ftsrg

TypeScript · 2 stars
ConcurrentWitness2Test
Sources of the ConcurrentWitness2Test violation witness validator tool

Python · 1 star
blockchain-benchmarks-tpcc
TPC-C benchmark implementations for blockchain platforms

Java · 0 stars

Beginner friendly Everything

Open All

Statement expression drops `reach_error()` (2SB, 4SB) Open

ftsrg/theta#575 · 1 assignee · Opened Sep 18, 2026
solver-z3 (Z3:new) produces unusable interpolants and crashes; legacy Z3 is unaffected Open

Difficulty 5/5 Over a week Newbie friendliness 35/100

ftsrg/theta#573 · Opened Sep 17, 2026
Mid-object pointer loses its offset across a non-inlined call, causing false valid-deref alarms (31 tasks, -496) Open

bug

Difficulty 5/5 Over a week Newbie friendliness 35/100

ftsrg/theta#571 · 1 comment · Opened Sep 12, 2026
OC backend reports Safe on a reachable NULL dereference when the alias graph is non-empty Open

bug

Difficulty 4/5 3-5 days Newbie friendliness 48/100

ftsrg/theta#570 · Opened Sep 12, 2026
Regression 7.3.0 -> 8.0.0: -2046 score, 1098 correct->timeout, 37 new no-overflow false alarms Open

Difficulty 5/5 Over a week Newbie friendliness 28/100

ftsrg/theta#564 · 6 comments · Opened Sep 10, 2026
Frontend: fesetround with a non-default rounding mode Open

Difficulty 3/5 1-2 days Newbie friendliness 65/100

ftsrg/theta#563 · Opened Sep 10, 2026
Frontend: typeof over an expression whose type cannot be determined Open

Difficulty 3/5 1-2 days Newbie friendliness 65/100

ftsrg/theta#562 · Opened Sep 10, 2026
Frontend: pthread handle base is not a reference variable Open

Difficulty 3/5 1-2 days Newbie friendliness 65/100

ftsrg/theta#561 · Opened Sep 10, 2026
Frontend: TypeUtils.cast type mismatch Open

Difficulty 4/5 3-5 days Newbie friendliness 42/100

ftsrg/theta#560 · Opened Sep 10, 2026
Frontend: assignment LHS is a BvAdd/BvPos expression Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

ftsrg/theta#559 · Opened Sep 10, 2026
Frontend: local mutex handles are unsupported Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

ftsrg/theta#558 · Opened Sep 10, 2026
Frontend: inlining refuses an arity mismatch between call site and procedure Open

Difficulty 4/5 3-5 days Newbie friendliness 35/100

ftsrg/theta#557 · Opened Sep 10, 2026
Frontend: non-constant dereference offset in a pthread handle Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

ftsrg/theta#555 · Opened Sep 10, 2026
Frontend: floating-point member of a byte-addressed union is unsupported Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

ftsrg/theta#554 · Opened Sep 10, 2026
Frontend: "No such variable or macro" on declared symbols Open

Difficulty 4/5 3-5 days Newbie friendliness 35/100

ftsrg/theta#553 · Opened Sep 10, 2026
IMC reports safe on 3 tasks where BMC/KIND/CEGAR find the counterexample Open

Difficulty 4/5 3-5 days Newbie friendliness 42/100

ftsrg/theta#552 · Opened Sep 10, 2026
Bitvector and integer arithmetic disagree, one wrong, on 5 tasks Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

ftsrg/theta#551 · Opened Sep 10, 2026
Unroll pass loop unroll order Open

ftsrg/theta#550 · 1 comment · 1 assignee · Opened Sep 9, 2026
Clone procedures for static thread creations to enable more simplification Open

ftsrg/theta#549 · 1 assignee · Opened Sep 9, 2026
Unroll busy wait loops Open

ftsrg/theta#548 · 1 assignee · Opened Sep 9, 2026
Thread-specific key support on the XCFA label Open

xcfa

Difficulty 5/5 Over a week Newbie friendliness 42/100

ftsrg/theta#544 · Opened Sep 8, 2026
Factor out ParseContext from analyses Open

xcfa

ftsrg/theta#543 · 1 assignee · Opened Sep 8, 2026
Bitvector pointer arithmetic issue Open

xcfa

ftsrg/theta#542 · 1 assignee · Opened Sep 7, 2026
Libvsync Open

xcfa

ftsrg/theta#541 · 3 comments · 2 assignees · Opened Sep 7, 2026
Fix config serialization Open

xcfa

ftsrg/theta#540 · 1 comment · 1 assignee · Opened Sep 5, 2026
Non-declaration-based mutex tracking Open

xcfa

ftsrg/theta#538 · 1 comment · 1 assignee · Opened Sep 3, 2026
Push-button full sv-benchmarks regression test with validation Open

xcfa

ftsrg/theta#535 · 2 assignees · Opened Aug 31, 2026
Expression simplifier for bitvectors Open

xcfa

ftsrg/theta#533 · 1 assignee · Opened Aug 31, 2026
CEGAR vs. OC verdict mismatch Open

xcfa

ftsrg/theta#532 · 2 comments · 1 assignee · Opened Aug 31, 2026
ldv-regression debugging Open

xcfa

ftsrg/theta#529 · 6 comments · 2 assignees · Opened Aug 25, 2026
aws-c-common wrong tasks debugging Open

xcfa

ftsrg/theta#528 · 2 comments · 1 assignee · Opened Aug 25, 2026
Create new benchmark portfolio Open

xcfa

ftsrg/theta#526 · 1 assignee · Opened Aug 25, 2026
Inspecting wrong verdicts one-by-one Open

xcfa

Difficulty 5/5 Over a week Newbie friendliness 20/100

ftsrg/theta#525 · 2 comments · Opened Aug 25, 2026
Sonar not reporting full test coverage Open

Difficulty 3/5 1-2 days Newbie friendliness 55/100

ftsrg/theta#514 · 1 comment · Opened Jun 17, 2026
Theta landing page Open

ftsrg/theta#510 · 1 assignee · Opened Jun 10, 2026
CHC-based interpolation issue Open

ftsrg/theta#509 · 1 assignee · Opened Jun 10, 2026
CI requests Open

Difficulty 4/5 3-5 days Newbie friendliness 42/100

ftsrg/theta#508 · Opened Jun 10, 2026
Inlining doesn't instantiate local variables Open

bug

Difficulty 3/5 1-2 days Newbie friendliness 72/100

ftsrg/theta#506 · 5 comments · Opened Jun 9, 2026
OC Checker: variable is not initialized Open

bug

ftsrg/theta#500 · 1 comment · 1 assignee · Opened May 21, 2026
PrimeMEPassValidator will not finish the validation in certain cases Open

bug core

ftsrg/theta#498 · 2 comments · 1 assignee · Opened May 12, 2026
`visitUnaryExpressionSizeOrAlignOf` does not handle `sizeof(struct Node)` Open

bug xcfa

ftsrg/theta#497 · 1 comment · 1 assignee · Opened May 11, 2026
Termination analysis: Bug for non-terminating nested loop Open

Difficulty 4/5 3-5 days Newbie friendliness 45/100

ftsrg/theta#496 · 1 comment · Opened May 7, 2026
Liveness CEGAR can cause StackOverflow, switch to queue-based recursion needed Open

bug

Difficulty 4/5 3-5 days Newbie friendliness 45/100

ftsrg/theta#490 · Opened Apr 16, 2026
Termination analysis: Bug Open

Difficulty 4/5 3-5 days Newbie friendliness 52/100

ftsrg/theta#482 · 7 comments · Opened Feb 16, 2026
Modular Termination Validation Disappeared Open

bug xcfa

ftsrg/theta#477 · 1 assignee · Opened Dec 18, 2025
MathSAT installation doesn't work on windows Open

bug

Difficulty 2/5 1-3 hours Newbie friendliness 38/100

ftsrg/theta#470 · 1 comment · Opened Dec 5, 2025
XSTS initialization at declaration not working Open

xsts

ftsrg/theta#467 · 1 comment · 1 assignee · Opened Dec 1, 2025
C frontend recursive struct parsing Open

bug

ftsrg/theta#459 · 2 assignees · Opened Nov 28, 2025
(XCFA) trace builder Open

xcfa

ftsrg/theta#457 · 4 assignees · Opened Nov 27, 2025
Refactor metadata & witness writer(s) Open

xcfa

ftsrg/theta#452 · 2 assignees · Opened Nov 24, 2025

ftsrg

Get new issues in your inbox