smackers/smackCatena di strumenti modulare per la verifica software che traduce LLVM IR nel linguaggio intermedio di verifica Boogie per il controllo di asserzioni bounded e unbounded sperimentali in programmi C.
SMACK è sia una toolchain modulare per la verifica del software che un verificatore software autonomo. Può essere usato per verificare le asserzioni nei suoi programmi di input. Nella sua modalità predefinita, le asserzioni vengono verificate fino a un dato limite sulle iterazioni dei cicli e sulla profondità di ricorsione; contiene anche supporto sperimentale per la verifica senza limiti. SMACK gestisce funzionalità complesse del linguaggio C, tra cui allocazione dinamica della memoria, aritmetica dei puntatori e operazioni bit a bit.
Sotto il cofano, SMACK è un traduttore dalla popolare rappresentazione intermedia (IR) del compilatore LLVM al linguaggio intermedio di verifica (IVL) Boogie. L'utilizzo dell'IR di LLVM sfrutta un numero crescente di front-end, ottimizzazioni e analisi dei compilatori. Attualmente SMACK supporta solo il linguaggio C tramite il compilatore Clang, anche se stiamo lavorando per fornire supporto per altri linguaggi. Il targeting di Boogie sfrutta una piattaforma canonica che semplifica l'implementazione di algoritmi per la verifica, il model checking e l'interpretazione astratta. Attualmente, SMACK si avvale dei verificatori Boogie e Corral.
Vedi sotto per requisiti di sistema, installazione, uso e tutto il resto.
Siamo molto interessati alla tua esperienza nell'uso di SMACK. Contatta Zvonimir, Michael o Shaobo per qualsiasi feedback.
Per domande generali, consulta prima le FAQ.
Se qualcosa è rotto o mancante, apri un issue.
Come ultima risorsa, invia una mail a Michael, Zvonimir e Shaobo.
Per rimanere informato sugli aggiornamenti, puoi guardare la pagina Github di SMACK.
Il progetto SMACK è stato parzialmente supportato da finanziamenti della National Science Foundation, VMware, Amazon e Microsoft Research. Ci affidiamo anche all'infrastruttura Emulab dell'Università dello Utah per un'ampia valutazione delle prestazioni di SMACK.
