Tools Developed by the Costa Group

• EthIR (Framework for high-level Analysis of Ethereum Bytecode)
• GASTAP (Gas-Aware Smart contracT Analysis Platform)
• GASOL (a Gas AnalysiS and Optimization tooL for Ethereum smart contracts)
• SuperStack (Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques)
• FORVES (FORmally VErified block optimizationS)
• FORVES 2.0 (FORmally VErified block optimizationS with Inter-Block Optimizations)
• FORYU (FORmal semantics for YUL in Coq)
• Circom (Compiler of the Circom Language)
• CIVER (Circuit Verification Tool)
• ZK‑ARCKIT (Analysis and Optimization of ZK Constraint Systems)

Tools developed but no longer maintained

• The SACO (Static Analyzer for Concurrent Objects) Tool
• The SYCO (Systematic Testing for Concurrent Objects) Tool
• The COSTA (Cost and Termination Analyzer) Tool
• The PUBS(Practical Upper Bound Solver) Tool
• The PET (Partial Evaluation-based Test Case Generator) Tool
• The COSTABS Tool
• DECO (DEadlock analyzer for Concurrent Objects) Tool
• MayPar (may-happen-in-parallel analyzer) Tool