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 36 reviews Date Reviewed 
  Model-based testing of probabilistic systems
Gerhold M., Stoelinga M.  Formal Aspects of Computing 30(1): 77-106, 2018. Type: Article

Gerhold and Stoelinga’s paper proposes an interesting framework to test probabilistic systems based on the concepts of soundness and completeness. The crux of their argument is “the conformance relation for probabilistic input/output c...

Apr 18 2018
  A compositional modelling and verification framework for stochastic hybrid systems
Wang S., Zhan N., Zhang L.  Formal Aspects of Computing 29(4): 751-775, 2017. Type: Article

The need to explore new formalisms for specifying, implementing, and verifying systems is driven by the increasing complexity of systems we wish to analyze and synthesize. At the same time, there is a growing realization of the need for techniques...

Mar 29 2018
  On partial state matching
Jančík P., Kofroň J.  Formal Aspects of Computing 29(5): 777-803, 2017. Type: Article

The code of a procedural-language computer program includes variables that have values at any given point during execution of that program. The state at a point of execution of a program includes the collection of values of all variables at that p...

Feb 28 2018
  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
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