Viorel Preoteasa

Inf. Comput., 2022

2020

The Refinement Calculus of Reactive Systems Toolset.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2020

2019

Mechanically Proving Determinacy of Hierarchical Block Diagram Translations.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019

Modelling Programmable Logic Controllers in Refinement Calculus of Reactive Systems.

[BibT_eX]

[DOI]

Timo Latvala

Kimmo Varpaaniemi

Proceedings of the 28th International Workshop on Concurrency, 2019

2017

Predictive runtime verification of timed properties.

[BibT_eX]

[DOI]

J. Syst. Softw., 2017

Predictive runtime enforcement.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

Type Inference of Simulink Hierarchical Block Diagrams in Isabelle.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2017

2016

A Nondeterministic and Abstract Algorithm for Translating Hierarchical Block Diagrams.

[BibT_eX]

[DOI]

CoRR, 2016

Compositional Semantics and Analysis of Hierarchical Block Diagrams.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software - 23rd International Symposium, 2016

Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Verifying Pointer Programs Using Separation Logic and Invariant Based Programming in Isabelle.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 12th International Conference, 2016

2015

Verification and code generation for invariant diagrams in Isabelle.

[BibT_eX]

[DOI]

Johannes Eriksson

J. Log. Algebraic Methods Program., 2015

Translating Hierarchical Block Diagrams into Composite Predicate Transformers.

[BibT_eX]

[DOI]

CoRR, 2015

2014

Refinement algebra with dual operator.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2014

Formalization of Refinement Calculus for Reactive Systems.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Refinement calculus of reactive systems.

[BibT_eX]

[DOI]

Proceedings of the 2014 International Conference on Embedded Software, 2014

2012

Invariant diagrams with data refinement.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2012

2011

Algebra of Monotonic Boolean Transformers.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2011

Lattice Properties.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2011

Semantics and proof rules of invariant based programs.

[BibT_eX]

[DOI]

Proceedings of the 2011 ACM Symposium on Applied Computing (SAC), TaiChung, Taiwan, March 21, 2011

2010

Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2010

Semantics and Data Refinement of Invariant Based Programs.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2010

2009

Frame rule for mutually recursive procedures manipulating pointers.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2009

Data Refinement of Invariant Based Programs.

[BibT_eX]

[DOI]

Proceedings of the 14th BCS-FACS Refinement Workshop, 2009

2006

Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the FM 2006: Formal Methods, 2006

2005

Pseudo-hoops.

[BibT_eX]

[DOI]

George Georgescu

Laurentiu Leustean

J. Multiple Valued Log. Soft Comput., 2005

An algebraic treatment of procedure refinement to support mechanical verification.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2005

2003

Reasoning about recursive procedures with parameters.

[BibT_eX]

[DOI]

Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, 2003

Reasoning about Pointers in Refinement Calculus.

[BibT_eX]

[DOI]

Xiaocong Fan

Proceedings of the 10th Asia-Pacific Software Engineering Conference (APSEC 2003), 2003

1999

A Relation Between Unambiguous Regular Expressions and Abstract Data Types.

[BibT_eX]

[DOI]