Related papers: Proceedings 18th Refinement Workshop
Refinement is one of the cornerstones of a formal approach to software engineering: the process of developing a more detailed design or implementation from an abstract specification through a sequence of mathematically-based steps that…
We are proud to present the papers from the 17th Refinement Workshop, co-located with FM 2015 held in Oslo, Norway on June 22nd, 2015. Refinement is one of the cornerstones of a formal approach to software engineering: the process of…
The 16th BCS-FACS Refinement Workshop was co-located with iFM 2013 held in Turku, Finland on June 11th, 2013. This volume contains the 6 papers selected for presentation at the workshop following a peer review process. The papers cover a…
Algorithmic and data refinement are well studied topics that provide a mathematically rigorous approach to gradually introducing details in the implementation of software. Program refinements are performed in the context of some programming…
The aim of the FESCA workshop is to bring together both young and senior researchers from formal methods, software engineering, and industry interested in the development and application of formal modelling approaches as well as associated…
These are the proceedings of the 14th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA). The workshop was held on April 22, 2017 in Uppsala (Sweden) as a satellite event to the European…
This volume contains the proceedings of F-IDE 2018, the fourth international workshop on Formal Integrated Development Environment, which was held as a FLoC 2018 satellite event, on July 14, 2018, in Oxford, England. High levels of safety,…
Model-driven design of software for safety-critical applications often relies on mathematically grounded techniques such as the B method. Such techniques consist in the successive applications of refinements to derive a concrete…
Traditionally, practitioners use formal methods pre-dominately for one half of the quality-assurance process: verification (do we build the software right?). The other half -- validation (do we build the right software?) -- has been given…
The aim of the FESCA workshop is to bring together junior researchers from formal methods, software engineering, and industry interested in the development and application of formal modelling approaches as well as associated analysis and…
Modularity is the fundamental aspect of modern software engineering, however many advanced modularity techniques requires prospective technologies as part of development and operation process. In this paper, we present Refinable Function,…
Refinement Reflection turns your favorite programming language into a proof assistant by reflecting the code implementing a user-defined function into the function's (output) refinement type. As a consequence, at uses of the function, the…
We introduce a new methodology based on refinement for testing the functional correctness of hardware and low-level software. Our methodology overcomes several major drawbacks of the de facto testing methodologies used in industry: (1) it…
Event-B is a formal approach oriented to system modeling and analysis. It supports refinement mechanism that enables stepwise modeling and verification of a system. By using refinement, the complexity of verification can be spread and…
Stepwise refinement of algebraic specifications is a well known formal methodology for program development. However, traditional notions of refinement based on signature morphisms are often too rigid to capture a number of relevant…
This paper discusses highly general mechanisms for specifying the refinement of a real-time system as a collection of lower level parallel components that preserve the timing and functional requirements of the upper level specification.…
Formal specification techniques allow expressing idealized specifications, which abstract from restrictions that may arise in implementations. However, partial implementations are universal in software development due to practical…
The aim of the FESCA workshop is to bring together junior researchers from formal methods, software engineering, and industry interested in the development and application of formal modelling approaches as well as associated analysis and…
Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable knob with which to inform the type system about what…
Software engineering concepts and processes are worthy of formal study; and yet we seldom formalize them. This "research ideas" article explores what a theory of software engineering could and should look like. Software engineering research…