Browse ORBilu by Open Access
- What it is and what it isn't
- Green Road / Gold Road?
- Ready to Publish. Now What?
- How can I support the OA movement?
- Where can I learn more?
ORBilu is a project developed by
   Automatic Repair and Deadlock Detection for Parameterized Systems; Sakr, Mouhammad  ; Volp, Marcus in Automatic Repair and Deadlock Detection for Parameterized Systems (2022, October 15) Detailed reference viewed: 16 (2 UL)The Reactive Synthesis Competition (SYNTCOMP): 2018-2021; ; 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) To verify or tolerate, that’s the questionPinto Gouveia, Ines ; Sakr, Mouhammad ; Graczyk, Rafal et alScientific 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: 71 (2 UL)AIGEN: Random Generation of Symbolic Transition SystemsSakr, Mouhammad ; in Sakr, Mouhammad; Jacobs, Swen (Eds.) AIGEN: Random Generation of Symbolic Transition Systems (2021, July 18) Detailed reference viewed: 68 (2 UL) |
||
