kframework/c-semantics on Hacker News

…- Cerberus Semantics https://www.cl.cam.ac.uk/~pes20/cerberus/ - https://github.com/kframework/c-semantics - https://github.com/TrustInSoft/tis-interpreter

comment by philzook · 2024-01-30 · in The C bounded model checker: criminally underused

…I no longer recall>?". There was a long pause, and then... "Yes." [1] https://kframework.org/ [2] https://github.com/kframework/c-semantics/tree/master/semant...

comment by mncharity · 2023-05-12 · in The Cerberus C semantics [pdf]

https://github.com/kframework/c-semantics while you can do static analysis with this the dynamic instrumentation of UB isnfar more thorough than ubsan

comment by yababa_y · 2022-12-01 · in Soufflé: A Datalog Synthesis Tool for Static Analysis

…Have a look at a formal description of it! (And compare to a truly simple language like e.g. LISP). https://github.com/kframework/c-semantics/tree/master/semant... In contrast some basic Lambda calculus language semantics fit 0.5 of a page…

comment by still_grokking · 2022-11-20 · in Mildly interesting quirks of C

…executable semantics for C with a GCC-like interface: http://www.kframework.org/index.php/Main_Page https://github.com/kframework/c-semantics That RV-Match builds on an open framework, does well on benchmarks (yeah skepticism here), and…

comment by nickpsecurity · 2018-09-30 · in In-Depth: Static Code Analysis (2011)

This is the same underlying tool that powers KCC and RVMatch. https://github.com/kframework/c-semantics https://runtimeverification.com/match/ Exactly what I’d hoped someone would do. Well, the first step anyway. The second step was doing…

comment by nickpsecurity · 2018-05-01 · in KRust: A Formal Executable Semantics of Rust

…check out Rosu et al's KCC: an executable, formal semantics of C that addresses undefined behavior. https://github.com/kframework/c-semantics/blob/master/README...

comment by nickpsecurity · 2018-04-24 · in What you get is what you C: Controlling side effects in mainstream C compilers [pdf]

…for C that does something like that. Runtime Verification Inc uses it for their bug-hunting tools. https://github.com/kframework/c-semantics http://fsl.cs.illinois.edu/pubs/ellison-rosu-2012-popl.pdf

comment by nickpsecurity · 2018-03-24 · in C for All

…I just find the K framework plus an executable, formal semantics for C cool as heck. :) https://github.com/kframework/c-semantics https://runtimeverification.com/match/ They also have an article comparing it to Tis-interpreter here:…

comment by nickpsecurity · 2018-02-19 · in Tis-interpreter: An interpreter for detecting undefined behavior in standard C

…K's tools or output using C-oriented tools. [1] http://www.kframework.org/index.php/Main_Page [2] https://github.com/kframework/c-semantics [3] https://runtimeverification.com/match/1.0-SNAPSHOT/docs/benc... [4]…

comment by nickpsecurity · 2018-01-15 · in IELE: A Formally-Specified VM for the Blockchain (2017)

I believe it is "simpler" in terms of formal semantics. Formalizing standard C is way harder (see https://github.com/kframework/c-semantics ). In fact, C0 is explicitly targeted at computer scientists rather than engineers.

comment by lou1306 · 2017-10-18 · in C0, an Imperative Programming Language for Novice Computer Scientists (2010) [pdf]

…use of these tools allowed them to make their C semantics executable in a style similar to GCC: https://github.com/kframework/c-semantics I want this group to do one for Rust and SPARK as a reference spec for certifying compilers for…

comment by nickpsecurity · 2017-07-26 · in Defining the Undefinedness of C (2015) [pdf]

…in Maude (esp K Framework) with one an executable, formal semantics for C done like a compiler: https://github.com/kframework/c-semantics

comment by nickpsecurity · 2017-07-21 · in Coq-based synthesis of Scala programs which are correct-by-construction [pdf]

…interpreter but not the development of complete semantics for C and specifically the k framework ( https://github.com/kframework/c-semantics ). Afaik, kcc is also really good at finding undefined behavior. Regehr even wrote about it in the…

comment by jpfr · 2017-07-05 · in Undefined Behavior in 2017

I presume that KCC in question is https://github.com/kframework/c-semantics , i.e., a formalization of C programming language in a form suitable for evaluation. It indeed can detect undefined behaviour, though last time I played with it (a…

comment by wuch · 2017-06-25 · in Getting compilers right: a reliable foundation for secure software

…runs in a framework on top of Maude rewrite engine. http://www.kframework.org/index.php/Main_Page https://github.com/kframework/c-semantics http://fsl.cs.illinois.edu/FSL/papers/2015/hathhorn-ellison-...

comment by nickpsecurity · 2017-06-15 · in System programming in Rust: beyond safety

…predicatable. A formal semantics of the language gives warnings whenever undefined behavior occurs. https://github.com/kframework/c-semantics

comment by jpfr · 2017-06-03 · in Convincing C programmers to switch to C++: A look at human behavior (2016)

…Then you get DDC for free plus a way to equivalence check reference compiler for certain features. https://github.com/kframework/c-semantics http://www.kframework.org/index.php/Main_Page

comment by nickpsecurity · 2017-05-16 · in Two years of Rust

…you verifying things about your application. If it even compiles, you have no undefined behavior. https://github.com/kframework/c-semantics On concurrency side, it's built on top of Maude tool that an inexperienced student was able to use…

comment by nickpsecurity · 2017-04-01 · in A semantic model for a substantial fragment of C

…suboptimal, but canonical) implementation. A good example of such a thing would be something like https://github.com/kframework/c-semantics

comment by sklogic · 2016-03-01 · in The Lisp Curse (2011)

…for C [0,1] and other mainstream languages [2] now. [0] http://robbertkrebbers.nl/thesis.html [1] https://github.com/kframework/c-semantics [2] http://www.kframework.org/index.php/Projects

comment by qznc · 2015-12-11 · in Why ML/OCaml are good for writing compilers (1998)

…formalize variadic function, float, bit field, setjmp/longjmp. All of them are formalized in KCC. https://github.com/kframework/c-semantics

comment by sanxiyn · 2015-11-30 · in The C standard formalized in Coq