Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Browse by topic Browse by titles Authors Reviewers Browse by issue Browse Help
Formal Aspects of Computing
  1-10 of 33 reviews Date Reviewed 
  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
Display per column
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2018 ThinkLoud, Inc.
Terms of Use
| Privacy Policy