Taxonomic Search: Industry
Results 1 - 10 of 102
Results
file
ABSTRACT
Multiprocessors are now so widespread that verification cannot ignore any longer the flavor of concurrency that they implement. Contrary to what most formal verification works assume, the execution model for concurrent programs is not Lamport's Sequential Consistency (SC), where an execution of a program corresponds to an interleaving of the instructions of the program.
file
ABSTRACT
Cyber-physical systems (CPS) are becoming an increasingly attractive target for adversaries to launch software attacks against. New approaches are needed to detect software-based vulnerabilities while meeting the constraints of embedded execution in CPS.
file
ABSTRACT
Malware analysis is one of the key problems in the realm of cybersecurity. Contemporary malware is nearly always protected from examination with the use of a “packer,” a program designed to obscure its malicious functionality. In the past, packers used techniques such as compression, encryption or time locks to thwart analysis.
file
ABSTRACT
Symbolic simulation is a powerful technique for building mathematical models describing a program’s results by simulating execution while interpreting inputs as symbolic variables. Such models can then be used to prove properties about the corresponding source program, including equivalence against a reference implementation.
file
The verification architecture of the Guardol system uses an implementation of HOL (Higher Order Logic) as a front end to SMT (Satisfiability Modulo Theories) technology. SMT provides high levels of proof automation. HOL provides semantic power, modelling the operational semantics of Guardol, an imperative language, and justifying the automatic deductive translation of programs to the functional form needed by SMT technology. In the Guardol system, extensive manipulation of programs and specifications is performed in HOL before goals are sent to the backend RADA SMT system.
