andreiarusoaie

Pinned Repositories

certified-procedure-coq
A Certified Procedure for Reachability Logic verification
0 2 00
certifying-unification-in-aml
This repo contains a series of Maude scripts for generating and checking proof certificates for syntactic unification in (Applicative) Matching Logic.
Language:Python0 3 00
findel-semantics-coq
A formal semantics of Findel in Coq.
Language:Coq0 1 00
investigating-smart-contracts-platforms
Investigate the opportunity of a Coq semantics of the Ethereum Virtual Machine.
1 2 00
itc-benchmarks
The modified static analysis benchmarks from Toyota ITC.
Language:C4 2 04
itc-testing-tools
This repo contains several scripts that can be used to run several static analysis tools over the ITC-Toyota benchmark.
Language:Python5 2 13
k
The K tools
Language:Java10
k-semantics
This repository includes the K specifications of the Alk language and of its dialects.
Language:Perl00
proof-generation-for-unification
A set of Coq proofs for (syntactic) unification in Matching Logic.
Language:Coq00
z3-ai-model-verification
This project contains several experiments using Z3 to verify artificial inteligence models.
Language:SMT1 2 00

andreiarusoaie's Repositories

andreiarusoaie/itc-testing-tools
This repo contains several scripts that can be used to run several static analysis tools over the ITC-Toyota benchmark.
Language:Python5 2 13
andreiarusoaie/itc-benchmarks
The modified static analysis benchmarks from Toyota ITC.
Language:C4 2 04
andreiarusoaie/investigating-smart-contracts-platforms
Investigate the opportunity of a Coq semantics of the Ethereum Virtual Machine.
1 2 00
andreiarusoaie/k
The K tools
Language:Java10
andreiarusoaie/z3-ai-model-verification
This project contains several experiments using Z3 to verify artificial inteligence models.
Language:SMT1 2 00
andreiarusoaie/certified-procedure-coq
A Certified Procedure for Reachability Logic verification
0 2 00
andreiarusoaie/certifying-unification-in-aml
This repo contains a series of Maude scripts for generating and checking proof certificates for syntactic unification in (Applicative) Matching Logic.
Language:Python0 3 00
andreiarusoaie/findel-semantics-coq
A formal semantics of Findel in Coq.
Language:Coq0 1 00
andreiarusoaie/k-semantics
This repository includes the K specifications of the Alk language and of its dialects.
Language:Perl00
andreiarusoaie/proof-generation-for-unification
A set of Coq proofs for (syntactic) unification in Matching Logic.
Language:Coq00
andreiarusoaie/unification-modulo-builtins
Unification modulo builtins in Maude: a prototype.
Language:Perl