China
Africa
Explore chapters and articles related to this topic
Modeling Guidelines of FreeRTOS in Event-B
Published in Ibrahiem M. M. El Emary, Anna Brzozowska, Shaping the Future of ICT, 2017
Eman H. Alkhammash, Michael J. Butler, Corina Cristea
Finally, there was an effort by Klein et al. [17,18] on the formal verification of the seL4 kernel starting with the abstract specification in higher-order logic, and finishing with its C implementation. The design approach is based on using the functional programming language Haskell [16] that provides an intermediate level that satisfies bottom-up and top-down approaches by providing a programming language for kernels developer and at the same time providing an artifact the can be automatically translated into the theorem prover. A formal model and C implementation are generated from the seL4 prototype designed in Haskell. The verification in Isabelle/HOL [24] shows that the implementation conforms with the abstract specification.
Reconstructor: a computer program that uses three-valued logics to represent lack of information in empirical scientific contexts
Published in Journal of Applied Non-Classical Logics, 2020
Also note that the same kinds of automatic calculations presented in this article can probably be carried out using other available software packages, based on different approaches. For example, the shallow semantical embeddings (SSE) approach utilises higher-order classical logic as a meta-logic, in which other object-level logics’ semantics are modelled; high-order logic theorem provers are then used to reason in the context of these object-logics (see Benzmüller, 2019 for an overview and some examples; one available software package for using this approach is Isabelle/HOL, see Nipkow, Paulson, & Wenzel, 2002). This approach has been fruitfully used within philosophy for studies in computational metaphysics (see Kirchner, Benzmüller & Zalta, 2019a, 2019b; and references therein).