Results 1 to 20 of 564
Sort by:

  • Risa/Asir
  • Referenced in 118 articles [sw00806]
  • algebraic engine is written mainly in C language and partly in assembler. It serves ... Asir has very similar syntax and semantics as C language. Furthermore, it has a debugger...

  • PHiPAC
  • Referenced in 53 articles [sw04898]
  • code blocks (if not removed, C semantics would prohibit many optimizations), and use of machine...

  • SatAbs
  • Referenced in 41 articles [sw12804]
  • SATABS: SAT-based predicate abstraction for ANSI-C. This paper presents a model checking tool ... model checker to handle the semantics of the ANSI-C standard accurately. This includes...

  • C-Light
  • Referenced in 12 articles [sw20973]
  • Verification-Oriented Language C-Light and Its Structural Operational Semantics. The paper presents the language ... library functions. The structural operational semantics of C-light in the Plotkin style is outlined...

  • Facile
  • Referenced in 22 articles [sw08679]
  • using a labeled transition system. Such a semantics is useful for reasoning about the operational ... Facile: theConcurrent and Functional Abstract Machine (C-FAM). The C-FAM executes concurrent processes evaluating ... expressions. The implementation semantics includes compilation rules from Facile to C-FAM instructions and execution...

  • KITTeL
  • Referenced in 9 articles [sw17045]
  • intermediate languages. Modeling the semantics of programming languages like C for the automated termination analysis ... much simpler semantics since most of the intricacies of C are taken care...

  • MPFR
  • Referenced in 232 articles [sw03312]
  • MPFR library is a C library for multiple-precision floating-point computations with correct rounding ... both efficient and has a well-defined semantics. It copies the good ideas from...

  • VeriSmall
  • Referenced in 6 articles [sw09788]
  • w.r.t. Leroy’s operational semantics for C minor. Thus when our VeriSmall static analyzer claims...

  • SeaHorn
  • Referenced in 19 articles [sw18274]
  • verification semantics to allow different levels of precision, (c) leverages the state...

  • LARCH
  • Referenced in 104 articles [sw02126]
  • variety of programming languages, including Ada, C, C++, CLU, CORBA, ML, Modula-3, and Smalltalk ... auxiliary specifications, written in LSL, to provide semantics for the primitive terms they use. Specifiers...

  • SAFECode
  • Referenced in 4 articles [sw13323]
  • describe a compilation strategy for standard C programs that guarantees that aggressive interprocedural pointer analysis ... necessary run-time checks in operational semantics and prove the correctness ... approach for a subset of C. Our semantics provide the foundation for other sophisticated static...

  • SymDiff
  • Referenced in 17 articles [sw13093]
  • agnostic tool for equivalence checking and displaying semantic (behavioral) differences over imperative programs. The tool ... exist from various source languages such as C, C# and x86. We discuss the tool...

  • CompCert
  • Referenced in 50 articles [sw09737]
  • code behaves exactly as prescribed by the semantics of the source program. By ruling ... result of the project is the CompCert C verified compiler, a high-assurance compiler...

  • CompCertS
  • Referenced in 3 articles [sw22722]
  • compiler using pointer as integer semantics. The CompCert C compiler provides the formal guarantee that ... this paper, we present a formally verified C compiler, CompCertS, which is essentially the CompCert ... stronger formal guarantee: it gives a semantics to more programs and ensures that the memory...

  • CompCertTSO
  • Referenced in 12 articles [sw08230]
  • consider the semantic design and verified compilation of a C-like programming language for concurrent ... memory) is also possible in the source semantics. We also describe some verified fence-elimination...

  • OTSL
  • Referenced in 3 articles [sw21005]
  • transition systems. By examples of formal semantics of C# statements, we illustrate the method...

  • KeY-C
  • Referenced in 5 articles [sw00486]
  • allows to prove partial correctness of C programs relative to pre- and postconditions ... give a glimpse of syntax, semantics, and calculus of C Dynamic Logic (CDL) that were...

  • Arlequin
  • Referenced in 5 articles [sw11442]
  • graphical interface written in C++, a more robust semantic analysis of input files...

  • ConArg2
  • Referenced in 6 articles [sw22084]
  • extension-based semantics in Abstract Argumentation. It exploits Gecode, an efficient C++ toolkit for developing...

  • GSGP
  • Referenced in 4 articles [sw18790]
  • C++ framework for geometric semantic genetic programming. Geometric semantic operators are new and promising genetic...