issues
search
ftsrg
/
theta
Generic, modular and configurable formal verification framework supporting various formalisms and algorithms
http://theta.inf.mit.bme.hu/
Apache License 2.0
49
stars
43
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Compare branches
#279
mondokm
closed
4 months ago
0
MDD-based analysis
#278
mondokm
closed
4 months ago
3
[AutoPR] Reformatted code
#277
thetabotmaintainer[bot]
closed
4 months ago
1
Clean zeta-merge branch
#276
mondokm
closed
4 months ago
0
This PR adds support for CHC solving via dedicated CHC solvers (including Z3)
#275
leventeBajczi
closed
4 months ago
2
MDD-based analysis
#274
mondokm
closed
4 months ago
1
`theta-analysis` depends on concrete solver implementations
#273
mondokm
opened
4 months ago
0
Enumtype smtlib
#272
RipplB
closed
4 months ago
2
SMTLIB integration fixes
#271
mondokm
closed
5 months ago
1
JavaSMT term transforming: inproper handling of function declarations
#270
RipplB
opened
5 months ago
3
[AutoPR] Reformatted code
#269
thetabotmaintainer[bot]
closed
5 months ago
1
Some solvers failing XstsTest
#268
RipplB
opened
5 months ago
11
PRED_SPLIT produces false negative results for XCFA
#267
leventeBajczi
opened
5 months ago
2
Initializers cannot use other global vars in c frontend
#266
leventeBajczi
opened
7 months ago
0
Allow "$" in XSTS variable names
#265
mondokm
closed
3 months ago
0
OC checker
#264
csanadtelbisz
closed
3 weeks ago
5
Improve local variables by introducing a new Decl for them
#263
mondokm
opened
8 months ago
1
[AutoPR] Reformatted code
#262
thetabotmaintainer[bot]
closed
8 months ago
1
Fix smtinterpol interpolation (#253)
#261
leventeBajczi
closed
8 months ago
2
Disabled llvm-related modules unless clang-15 is installed
#260
leventeBajczi
closed
8 months ago
2
Enhance PR messaging for checks
#259
leventeBajczi
closed
8 months ago
1
Adding JavaSMT support
#258
leventeBajczi
closed
8 months ago
3
Floating point type sometimes reports a significand of size N + 1 instead of N
#257
leventeBajczi
opened
8 months ago
0
Docker update
#256
leventeBajczi
closed
8 months ago
1
Updated actions to fix release message, docker push
#255
leventeBajczi
closed
8 months ago
1
Z3 update
#254
leventeBajczi
closed
8 months ago
4
Sequence interpolation with SMTInterpol
#253
RipplB
closed
8 months ago
0
C frontend fix
#252
leventeBajczi
closed
5 months ago
2
Added multi formalism to create product of arbitrary number of formal…
#251
RipplB
closed
5 months ago
5
Deploy doc only on master, test always
#250
leventeBajczi
closed
9 months ago
2
Configuration rules
#249
csanadtelbisz
closed
1 week ago
0
Xcfa COI SPIN artifact code
#248
csanadtelbisz
closed
10 months ago
0
General/instance vars in precision
#247
s0mark
opened
1 year ago
0
Log level affects Z3 behavior
#246
s0mark
opened
1 year ago
0
Urgent init location in XTA
#245
szdan97
opened
1 year ago
0
Interprocedural verification enhancement
#244
s0mark
closed
1 year ago
4
K induction and IMC
#243
leventeBajczi
closed
1 year ago
2
Fix concurrency witnesses
#242
AdamZsofi
closed
1 week ago
0
Adding smoke test to xcfa-cli
#241
leventeBajczi
closed
1 year ago
2
Adds support for the react-based interactive debugger
#240
leventeBajczi
closed
1 year ago
1
Pointer support
#239
sisakb
closed
9 months ago
5
ARG equals/hashCode fix
#238
leventeBajczi
closed
1 year ago
5
Update existing well-established solvers
#237
as3810t
closed
1 year ago
1
Pointers + data race
#236
csanadtelbisz
closed
1 week ago
0
Data race detection fixes
#235
csanadtelbisz
closed
1 year ago
0
Added code from CHC2C implementation
#234
leventeBajczi
closed
1 year ago
3
Xcfa phased procedure pass optimization + unsupported initializer
#233
csanadtelbisz
closed
1 year ago
0
WIP: Choice-else branch support
#232
arminzavada
closed
2 months ago
2
COI (abstract data-flow-based statement simplification)
#231
csanadtelbisz
closed
1 year ago
0
Harmonize integer div/mod semantics
#230
s0mark
closed
1 year ago
1
Previous
Next