The release identifier faidros is derived from the Greek name Φαιδρος (Phaidros) and means “bright”.
libtptp
which provides a TPTP parser, code emitter, and evaluation transformation towards Z3.
By annotating CASM functions with the attribute symbolic
allows the CASM symbolic execution to derive first order formula based TPTP traces of the desired annotated functions.
Furthermore, we support the complete building by (open-)source of the three main applications casmd
, casmf
, and casmi
and the corresponding libraries like libcasm-fe
or libcasm-ir
.
Language | We enabled the symbolic attribute for function definition language elements to annotate functions that shall be symbolically evaluated during the concolic execution. |
|
Application | Provided a new command line option (-s ) to the CASM interpreter application casmi to evaluate CASM specifications with the new concolic execution. |
|
Application | Enabled the concolic execution support in the CASM language server daemon application casmd for LSP-based editor integration to invoke concolic executions. |
|
Plug-in | Integrated a new LSP command in the monaco editor extension to invoke CASM concolic executions and render the generated TPTP trace. |
|
Environment | Full open-source based compilations of libraries and applications. | |
The release identifier epiktetos is derived from the Greek name Επικτητος (Epiktetos) and means “newly acquired”.
using
path namespace concept to make symbols visible and shorted their symbol name path.
Besides the using
path syntax, we support the local
rule definition now.
This rule allows a specifier to defined (nested) local state functions inside given rule scopes.
Language | We introduced a new language syntax definition element to make module symbols visible under shorter name. | |
Language | Provided support for the local rule to defined nested local states. | |
The release identifier diodoros is derived from the Greek name Διοδωρος (Diodoros) and means “gift of Zeus”.
import
syntax it is possible to load external specifications and modules into the current specification.
Second, the CASM language allows UTF-8 symbols in comments, string literals, and certain characters for identifier names.
Last but not least, we changed the init
definition to be optional in CASM specifications to support import
only specifications as well.
Language | We introduced a new language syntax definition element to specify the import of specifications and modules. |
|
Language | The CASM language front-end lexer does support UTF-8 characters now. | |
Language | Specifications can have optional init definition. |
|
The release identifier chares is derived from the Greek word Χαρης (Chares) and χαρις (Charis) and means “grace, kindness”.
casmf
.
This application function in the near future as the official CASM formatting application.
Second, another contribution provides 100% coverage of all LSP messages and structures (see libstdhl
) so that our casmd
can implement one language feature after the next one.
Last but not least, we continued with our own libtptp
implementation to prepare already the next steps for the CASM symbolic execution.
Application | Introducing the CASM source format and beautifier command line application called casmf based on the new lossless syntax representation |
|
Environment | LSP implementation covers 100% of the specification in libstdhl . |
|
Environment | Improvements in the libstdhl implementation state. |
|
The release identifier berenice is derived from the Greek word Βερενικη (Berenike, or Berenice) and means “bringing victory”.
casmi
.
Second, our huge effort over the summer has finally paid off. Now we are able to compile the CASM project more or less platform independent with various C++ compilers.
Therefore, we support and ship pre-compiled x86_64
binaries for Linux
, Mac
, and Windows
.
Third, besides the interpreter we ship a new daemon application called casmd
, which is our own server-sided Language Server Protocol (LSP) implementation to interact with LSP (editor) clients.
Last but not least, we publish our own LSP client plug-in extension for the monaco
editor framework. With this plug-in a fully functional CASM editor environment allows you to specify, debug, and run (execute) the provided CASM specification.
Language | We introduced a new language syntax definition element to specify global invariant conditions in CASM specifications. | |
Environment | Platform independent compilation supported to build x86_64 compatible 64-bit binaries for Linux , Mac , and Windows . |
|
Application | Introducing the CASM language server/service daemon command line application called casmd to interact with LSP clients. |
|
Plug-in | Integrated a LSP client as monaco editor extension provided as a CASM language environment service. |
|
The release identifier auxentios is derived from the Greek word αυξανω (auxano) and means “to increase, to grow”.
casmi
.
For now, we only support Linux
and ship a statically build x86_64
compatible 64-bit binary with zero dependencies.
The binary sources are packed and deployed to various environments including ArchLinux AUR and Docker.
Language | Contains the first version of the offical CASM language syntax, which contains the core elements of an ASM language implementation. | |
Environment | This release supports building x86_64 compatible 64-bit binaries for Linux -based operating systems. |
|
Application | Introducing the CASM interpreter command line application called casmi to numerically execute (simulate) CASM specification. |