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 |