| a |
| Abstract State Machines | SMT for state-based formal methods: the ASM case study |
| Automated Model Verification and Validation | More Automated Formal Methods?! If so, why, where & how? |
| Automatic transformation of programs | Salsa: An Automatic Tool to Improve the Numerical Accuracy of Programs |
| c |
| code generation | A Brief Introduction to the PVS2C Code Generator |
| d |
| dimensional analysis | The Measurement Library: Representing Physical Types in PVS |
| e |
| Equality Reasoning | On Conflict-Driven Reasoning |
| executable specifications | A Brief Introduction to the PVS2C Code Generator |
| f |
| floating-point arithmetic | Salsa: An Automatic Tool to Improve the Numerical Accuracy of Programs |
| Floating-point Round-off Error | Moving the Needle on Rigorous Floating-Point Precision Tuning |
| formal methods | More Automated Formal Methods?! If so, why, where & how?
The MINERVA Software Development Process |
| formal verification | The Measurement Library: Representing Physical Types in PVS
The MINERVA Software Development Process |
| m |
| mixed-precision tuning | Moving the Needle on Rigorous Floating-Point Precision Tuning |
| model animation | The MINERVA Software Development Process |
| Model Based Systems Engineering | More Automated Formal Methods?! If so, why, where & how? |
| model building | On Conflict-Driven Reasoning |
| n |
| Numerical accuracy | Salsa: An Automatic Tool to Improve the Numerical Accuracy of Programs |
| p |
| program analysis | Moving the Needle on Rigorous Floating-Point Precision Tuning |
| proof certificates | Moving the Needle on Rigorous Floating-Point Precision Tuning |
| r |
| real-world types | The Measurement Library: Representing Physical Types in PVS |
| refinement proof | SMT for state-based formal methods: the ASM case study |
| Rigorous Global Optimization | Moving the Needle on Rigorous Floating-Point Precision Tuning |
| runtime verification | SMT for state-based formal methods: the ASM case study |
| s |
| Satisfiability modulo assignment | On Conflict-Driven Reasoning |
| Satisfiability Modulo Theory | On Conflict-Driven Reasoning |
| SMT solver | SMT for state-based formal methods: the ASM case study |
| software development | The MINERVA Software Development Process |
| software validation | The MINERVA Software Development Process |
| specification language | A Brief Introduction to the PVS2C Code Generator |
| static analysis | Salsa: An Automatic Tool to Improve the Numerical Accuracy of Programs |
| t |
| theorem proving | On Conflict-Driven Reasoning |
| theory combination | On Conflict-Driven Reasoning |
| y |
| Yices | SMT for state-based formal methods: the ASM case study |
