Abstract is missing.
- SARL: OO Framework Specification for Static AnalysisPietro Ferrara, Luca Negrini. 3-20 [doi]
- QPR Verify: A Static Analysis Tool for Embedded Software Based on Bounded Model CheckingMarko Kleine Büning, Carsten Sinz, David Faragó. 21-32 [doi]
- Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIXVadim Zaliva, Ilia Zaichuk, Franz Franchetti. 33-49 [doi]
- Automatic Detection and Repair of Transition- Based Leakage in Software BinariesKonstantinos Athanasiou, Thomas Wahl, A. Adam Ding, Yunsi Fei. 50-67 [doi]
- BanditFuzz: A Reinforcement-Learning Based Performance Fuzzer for SMT SolversJoseph Scott, Federico Mora, Vijay Ganesh. 68-86 [doi]
- Synthesis of Solar Photovoltaic Systems: Optimal Sizing ComparisonAlessandro Trindade, Lucas C. Cordeiro. 87-105 [doi]
- Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly LanguageJay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel. 106-123 [doi]
- MCBAT: Model Counting for Constraints over Bounded Integer ArraysAbtin Molavi, Tommy Schneider, Mara Downing, Lucas Bang. 124-143 [doi]
- Verification of an Optimized NTT AlgorithmJorge A. Navas, Bruno Dutertre, Ian A. Mason. 144-160 [doi]
- Can We Avoid Rounding-Error Estimation in HPC Codes and Still Get Trustworthy Results?Fabienne Jézéquel, Stef Graillat, Daichi Mukunoki, Toshiyuki Imamura, Roman Iakymchuk. 163-177 [doi]
- An Efficient Floating-Point Bit-Blasting API for Verifying C ProgramsMikhail R. Gadelha, Lucas C. Cordeiro, Denis A. Nicole. 178-195 [doi]
- Rigorous Enclosure of Round-Off Errors in Floating-Point ComputationsRémy Garcia, Claude Michel, Michel Rueher. 196-212 [doi]
- Towards Numerical Assistants - Trust, Measurement, Community, and Generality for the Numerical WorkbenchPavel Panchekha, Zachary Tatlock. 213-220 [doi]
- Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive InvariantsBibek Kabi, Eric Goubault, Antoine Miné, Sylvie Putot. 221-238 [doi]