w/in this Title
Formal Aspects of Computing
1-10 of 33 reviews
Designing a semantic model for a wide-spectrum language with concurrency
Colvin R., Hayes I., Meinicke L. Formal Aspects of Computing 29(5): 853-875, 2017. Type: Article
A concurrent wide-spectrum language combines a concurrent programming language with specification constructs. Colvin et al. provide a unified framework for defining the semantics of such languages. The semantics is trace-based and captures program...
Jan 10 2018
Incremental bounded model checking for embedded software
Schrammel P., Kroening D., Brain M., Martins R., Teige T., Bienmüller T. Formal Aspects of Computing 29(5): 911-931, 2017. Type: Article
Bounded model checking is employed in tools for the formal verification of C programs such as the C bounded model checker (CBMC). The key idea of this technique is to unwind unbounded program loops to a fixed depth and to translate the resulting p...
Dec 4 2017
Partial evaluation of string obfuscations for Java malware detection
Chawdhary A., Singh R., King A. Formal Aspects of Computing 29(1): 33-55, 2017. Type: Article
Cyber security has become a major concern in government, industry, and academia and in the everyday lives of individuals. How we secure our information systems and maintain the privacy and integrity of our online presence and data is a significant...
Oct 2 2017
Transforming Boolean equalities into constraints
Antoy S., Hanus M. Formal Aspects of Computing 29(3): 475-494, 2017. Type: Article
In declarative programming languages, a variable is a symbol representing a value determined by computational rules rather than a space in memory. The two main forms of declarative languages are functional and logic. In functional languages, varia...
Sep 13 2017
Manifest domains: analysis and description
Bjørner D. Formal Aspects of Computing 29(2): 175-225, 2017. Type: Article
Dines Bjørner in numerous publications suggested a triptych view of software engineering, specified in this paper as follows: “before hardware and software systems can be designed and coded, we must have a reasonable grasp of ‘its̵...
Aug 11 2017
Proof checking and logic programming
Miller D. Formal Aspects of Computing 29(3): 383-399, 2017. Type: Article
A proof checker is a program that takes a claimed proof of a logic formula and decides whether this claim is true; in applications such as program verification and automated reasoning, it is thus not necessary to trust the (potentially big) prover...
Jun 27 2017
Foundations for using linear temporal logic in Event-B refinement
Hoang T., Schneider S., Treharne H., Williams D. Formal Aspects of Computing 28(6): 909-935, 2016. Type: Article
Event-B is a formal method for system-level modeling and analysis. In the last decade, Event-B refinement has generated a lot of interest as a formalism for developing highly reliable software. The Event-B language, along with tools such as Rodin ...
Apr 12 2017
Model checking learning agent systems using Promela with embedded C code and abstraction
Kirwan R., Miller A., Porr B. Formal Aspects of Computing 28(6): 1027-1056, 2016. Type: Article
Model checking is a formal method that decides whether a system satisfies a property formulated in temporal logic. While model checking is typically applied to hardware/software systems, it may be used to analyze any system that reaches only finit...
Mar 29 2017
Model checking Petri nets with names using data-centric dynamic systems
Montali M., Rivkin A. Formal Aspects of Computing 28(4): 615-641, 2016. Type: Article
Carl Adam Petri established Petri net theory, in 1962, with the publication of his doctoral thesis, “Kommunikation mit Automaten.” In the following 54 years, a rich and extensive body of work has been added to the theory and language c...
Mar 10 2017
Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
Aransay J., Divasón J. Formal Aspects of Computing 28(6): 1005-1026, 2016. Type: Article
Formalization is rapidly evolving from being highly desirable but thought too difficult to be realistic, to being quite feasible and well on its way to being expected. The raw technology of theorem provers certainly is ready. What is still evolvin...
Mar 9 2017
Reproduction in whole or in part without permission is prohibited. Copyright © 2000-2018 ThinkLoud, Inc.