AFM17:Keyword Index

KeywordPapers
A
Abstract State MachinesSMT for state-based formal methods: the ASM case study
Automated Model Verification and ValidationMore Automated Formal Methods?! If so, why, where & how?
Automatic transformation of programsSalsa: An Automatic Tool to Improve the Numerical Accuracy of Programs
C
code generationA Brief Introduction to the PVS2C Code Generator
D
dimensional analysisThe Measurement Library: Representing Physical Types in PVS
E
Equality ReasoningOn Conflict-Driven Reasoning
executable specificationsA Brief Introduction to the PVS2C Code Generator
F
floating-point arithmeticSalsa: An Automatic Tool to Improve the Numerical Accuracy of Programs
Floating-point Round-off ErrorMoving the Needle on Rigorous Floating-Point Precision Tuning
formal methodsMore Automated Formal Methods?! If so, why, where & how?
The MINERVA Software Development Process
formal verificationThe Measurement Library: Representing Physical Types in PVS
The MINERVA Software Development Process
M
mixed-precision tuningMoving the Needle on Rigorous Floating-Point Precision Tuning
model animationThe MINERVA Software Development Process
Model Based Systems EngineeringMore Automated Formal Methods?! If so, why, where & how?
model buildingOn Conflict-Driven Reasoning
N
Numerical accuracySalsa: An Automatic Tool to Improve the Numerical Accuracy of Programs
P
program analysisMoving the Needle on Rigorous Floating-Point Precision Tuning
proof certificatesMoving the Needle on Rigorous Floating-Point Precision Tuning
R
real-world typesThe Measurement Library: Representing Physical Types in PVS
refinement proofSMT for state-based formal methods: the ASM case study
Rigorous Global OptimizationMoving the Needle on Rigorous Floating-Point Precision Tuning
runtime verificationSMT for state-based formal methods: the ASM case study
S
Satisfiability modulo assignmentOn Conflict-Driven Reasoning
Satisfiability Modulo TheoryOn Conflict-Driven Reasoning
SMT solverSMT for state-based formal methods: the ASM case study
software developmentThe MINERVA Software Development Process
software validationThe MINERVA Software Development Process
specification languageA Brief Introduction to the PVS2C Code Generator
static analysisSalsa: An Automatic Tool to Improve the Numerical Accuracy of Programs
T
theorem provingOn Conflict-Driven Reasoning
theory combinationOn Conflict-Driven Reasoning
Y
YicesSMT for state-based formal methods: the ASM case study