• There are IDEs for KeY, including an Eclipse extension, that make it easy to keep track of
proof obligations in larger projects [Hentschel et al., 2014c].• A stripped down version of …

Given data drawn from a mixture of multivariate Gaussians, a basic problem is to accurately
estimate the mixture parameters. We give an algorithm for this problem that has running time …

A central objective of the verifying compiler grand challenge is to develop a push-button
verifier that generates proofs of correctness in a syntax-driven fashion similar to the way an …

More than 20 years of research has created a large body of ideas, concepts, and theories for
model-based development of embedded software-intensive systems. These approaches …

Coordinating the interactions of applications running on the diversity of both mobile and
embedded devices that will be common in ubiquitous computing environments is still a …

Model driven development (MDD) is an emerging paradigm for software construction that
uses models to specify programs, and model transformations to synthesize executables …

An ongoing challenge for computer science is the development of a tool which automatically
verifies programs meet their specifications, and are free from runtime errors such as divide …

Formal methods have emerged as an alternative approach to ensuring quality and
correctness of highly critical systems, overcoming limitations of traditional validation …

摘要形式化方法是构建可信软件的重要途径. 基于对算法问题的分析, 针对形式化方法PAR
开发算法的特征, 刻划了问题分划, 递推关系构造方面的规律. 从一类问题的形式化功能规约出发 …

A goal of software product lines is the economical assembly of programs in a family of
programs. In this paper, we explore how theorems about program properties may be …