Downloads provided by UsageCounts
Isabelle/C is a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE development environment. Our framework provides an abstract interface for verification back-ends to be plugged-in independently. Thus, various techniques such as deductive program verification or white-box testing can be applied to the same source, which is part of an integrated Isabelle/PIDE document model. Semantic back-ends are free to choose the supported C fragment and its semantics. In particular, they can differ on the chosen memory model or the specification mechanism for e.g. framing conditions. Isabelle/C is itself an entry in the AFP. Via this site, we distribute a bundle of Isabelle/C with two semantic backends, together with example suites for Isabelle/C as such. Moreover, each semantic backend comes with its own example suites: Isabelle/C/AutoCorres (The integration of l4v into Isabelle/C is based on revision e3352826893db4d00fc402fad2a0125307ebe45e in the seL4-project) Isabelle/C/Clean (The integration of Isabelle/Clean is based on the Isabelle2021-1 AFP version and is in the current version still experimental). The Isabelle/C framework supports semantic annotations of C sources in the form of comments. Annotations serve to locally control back-end settings, and can express the term focus to which an annotation refers. Both the logical and the syntactic context are available when semantic annotations are evaluated. As a consequence, a formula in an annotation can refer both to HOL or C variables. The project is linked to general website containing links to videos and papers; developers may be interested in our git-repo (select current branch: C_2021-1). CAVEAT: The session Isabelle_C_AutoCorres does not work under Windows due to intern restrictions of AutoCorres.
Deductive Program Verification, Isabelle/HOL, C11
Deductive Program Verification, Isabelle/HOL, C11
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
| views | 40 | |
| downloads | 19 |

Views provided by UsageCounts
Downloads provided by UsageCounts