References of "Sakr, Mouhammad 50044098"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailAutomatic Repair and Deadlock Detection for Parameterized Systems
Jacobs, Swen; Sakr, Mouhammad UL; Volp, Marcus UL

in Automatic Repair and Deadlock Detection for Parameterized Systems (2022, October 15)

Detailed reference viewed: 11 (0 UL)
See detailThe Reactive Synthesis Competition (SYNTCOMP): 2018-2021
Jacobs, Swen; Perez, Guillermo; Abraham et al

Report (2022)

We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then, we introduce new ... [more ▼]

We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then, we introduce new benchmark classes that have been added to the SYNTCOMP library and give an overview of the participants of SYNTCOMP. Finally, we present and analyze the results of our experimental evaluations, including a ranking of tools with respect to quantity and quality of solutions. [less ▲]

Detailed reference viewed: 14 (0 UL)
Full Text
Peer Reviewed
See detailTo verify or tolerate, that’s the question
Pinto Gouveia, Ines UL; Sakr, Mouhammad UL; Graczyk, Rafal UL et al

Scientific Conference (2021, December 06)

Formal verification carries the promise of absolute correctness, guaranteed at the highest level of assurance known today. However, inherent to many verification attempts is the assumption that the ... [more ▼]

Formal verification carries the promise of absolute correctness, guaranteed at the highest level of assurance known today. However, inherent to many verification attempts is the assumption that the underlying hardware, the code-generation toolchain and the verification tools are correct, all of the time. While this assumption creates interesting recursive verification challenges, which already have been executed successfully for all three of these elements, the coverage of this assumption remains incomplete, in particular for hardware. Accidental faults, such as single-event upsets, transistor aging and latchups keep causing hardware to behave arbitrarily in situations where such events occur and require other means (e.g., tolerance) to safely operate through them. Targeted attacks, especially physical ones, have a similar potential to cause havoc. Moreover, faults of the above kind may well manifest in such a way that their effects extend to all software layers, causing incorrect behavior, even in proven correct ones. In this position paper, we take a holistic system-architectural point of view on the role of trusted-execution environments (TEEs), their implementation complexity and the guarantees they can convey and that we want to be preserved in the presence of faults. We find that if absolute correctness should remain our visionary goal, TEEs can and should be constructed differently with tolerance embedded at the lowest levels and with verification playing an essential role. Verification should both assure the correctness of the TEE construction protocols and mechanisms as well as help protecting the applications executing inside the TEEs. [less ▲]

Detailed reference viewed: 66 (2 UL)
Full Text
Peer Reviewed
See detailAIGEN: Random Generation of Symbolic Transition Systems
Sakr, Mouhammad UL; Jacobs, Swen

in Sakr, Mouhammad; Jacobs, Swen (Eds.) AIGEN: Random Generation of Symbolic Transition Systems (2021, July 18)

Detailed reference viewed: 62 (2 UL)