GULF
发表于 2025-3-28 16:38:40
Sound Symbolic Linking in the Presence of Preprocessingcation of different pieces of an application in separation. We propose symbolic linking as such a modular approach, since it allows to decide whether or not earlier verified source files can be safely linked together (i.e. earlier proven properties remain valid)..If an annotation-based verifier for
知识
发表于 2025-3-28 19:05:58
Inferring Physical Units in B Models for annotating variables with (physical) units of measurement. There is thus no obvious way to reason about correct or incorrect usage of such units. In this paper we present a technique that analyses the usage of physical units throughout a B machine, infers missing units and notifies the user of
myriad
发表于 2025-3-29 01:31:27
http://reply.papertrans.cn/88/8709/870813/870813_43.png
解冻
发表于 2025-3-29 04:29:07
A Type System for Componentst is difficult to guarantee that such modifications will not disrupt ongoing computations. In a previous paper, a solution to this problem was proposed by extending the object-oriented language ABS with a component model allowing the programmer to: .) perform updates on objects by means of . and the
有害处
发表于 2025-3-29 07:22:56
Early Fault Detection in DSLs Using SMT Solving and Automated Debugging validate a wide range of properties, classified into basic and advanced. Basic validation includes syntax checking, reference checking and type checking. Advanced validation concerns domain specific properties related to the semantics of the DSL. For verification, we mechanically translate the DSL
eulogize
发表于 2025-3-29 14:47:43
Static Detection of Implementation Errors Using Formal Code Specificationctional errors. In this work, we investigate the impact of various levels of formal specification on the ability to statically detect errors in code. Our goal is to quantify the return on investment with regards to the effectiveness of identifying errors versus the overhead of specifying software at
interlude
发表于 2025-3-29 19:19:59
http://reply.papertrans.cn/88/8709/870813/870813_47.png
diskitis
发表于 2025-3-29 23:39:33
{,} as a Test Case Generator for the Test Template Frameworkoperations for set management. As such, it can find solutions of first-order logic formulas involving set-theoretic operators. The Test Template Framework (TTF) is a model-based testing method for the Z notation. In the TTF, test cases are generated from test specifications, which are predicates wri
Thymus
发表于 2025-3-30 03:58:14
Zero Overhead Runtime Monitoringam violates some property. Runtime monitoring is in particular important when an exhaustive formal verification fails. While the approach allows for a safe execution of programs, it may impose a significant runtime overhead..In this paper, we propose a novel technique combining verification and moni
STIT
发表于 2025-3-30 07:23:27
Run-Time Verification of Coboxesently running object groups (coboxes) in SAGA (Software trace Analysis using Grammars and Attributes) which is a run-time checker that provides a smooth integration of the specification and the efficient run-time checking of both data- and protocol-oriented properties of message sequences. We illust