Abstraction-Based Malware Analysis Using Rewriting and Model Checking.

Philippe Beaucamps Isabelle Gnaedig Jean-Yves Marion

Published in: ESORICS (2012)

Keyphrases

model checking
temporal logic
dynamic analysis
abstract interpretation
formal verification
model checker
finite state
temporal properties
symbolic model checking
static analysis
verification method
transition systems
linear temporal logic
bounded model checking