Burkhart Wolff
53
Documents
Présentation
[https://www.lri.fr/~wolff/](https://www.lri.fr/~wolff/ "Home Page at UPSud / LRI")
[https://www.lri.fr/~wolff/](https://www.lri.fr/~wolff/ "Home Page at UPSud / LRI")
Publications
- 14
- 7
- 7
- 6
- 5
- 4
- 4
- 4
- 4
- 4
- 4
- 3
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
Operational Semantics formally proven in HOL-CSPArchive of Formal Proofs, 2023, https://isa-afp.org/entries/HOL-CSP_OpSem.html
Article dans une revue
hal-04503764v1
|
|
HOL-CSPM - Architectural operators for HOL-CSPArchive of Formal Proofs, 2023, https://www.isa-afp.org/entries/HOL-CSPM.html
Article dans une revue
hal-04503778v1
|
|
Modeling and analysing Cyber–Physical Systems in HOL-CSPRobotics and Autonomous Systems, 2023, 170, pp.104549. ⟨10.1016/j.robot.2023.104549⟩
Article dans une revue
hal-04265879v1
|
|
The HOL-CSP Refinement ToolkitArchive of Formal Proofs, 2020, https://www.isa-afp.org/entries/CSP_RefTK.html#cite-popup
Article dans une revue
hal-04503821v1
|
|
A Sound Type System for Physical Quantities, Units, and MeasurementsArchive of Formal Proofs, 2020, https://www.isa-afp.org/entries/Physical_Quantities.html#
Article dans une revue
hal-04503812v1
|
|
|
|
Timed Discrete-Event Simulation of Aviation ScenariosSNE Simulation Notes Europe, 2020, 30 (2), pp.51-60. ⟨10.11128/sne.30.tn.10512⟩
Article dans une revue
hal-02881889v1
|
Model Transformation as Conservative Theory-Transformation.The Journal of Object Technology, 2020, 19 (3), pp.3:1. ⟨10.5381/jot.2020.19.3.a3⟩
Article dans une revue
hal-04500112v1
|
|
HOL-CSP Version 2.0Archive of Formal Proofs, 2019, https://www.isa-afp.org/entries/HOL-CSP.html#
Article dans une revue
hal-04503825v1
|
|
A Formal Development of a Polychronous Polytimed Coordination LanguageArchive of Formal Proofs, 2019, https://www.isa-afp.org/entries/TESL_Language.html
Article dans une revue
hal-04495414v1
|
|
Deeply Integrating C11 Code Support into Isabelle/PIDEEPTCS, 2019, 310, pp.13-28. ⟨10.48550/arXiv.1912.10630⟩
Article dans une revue
hal-04500151v1
|
|
Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of PathsArchive of Formal Proofs, 2016
Article dans une revue
hal-01764577v1
|
|
Symbolic Test-generation in HOL-TestGen/CirTA: A Case StudyInternational Journal of Software and Informatics (IJSI), 2015
Article dans une revue
hal-01765531v1
|
|
Formal Firewall Conformance TestingJournal of Software Testing, Verification and Reliability, 2015, 25 (1), pp.34-71. ⟨10.1002/stvr.1544⟩
Article dans une revue
hal-01213717v1
|
|
A Meta-Model for the Isabelle APIArchive of Formal Proofs, 2015
Article dans une revue
hal-01214254v1
|
|
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5Archive of Formal Proofs, 2014
Article dans une revue
hal-01214252v1
|
|
On Theorem-proving based TestingFormal Aspects of Computing, 2013, 25 (5), pp.683-721. ⟨10.1007/s00165-012-0222-y⟩
Article dans une revue
hal-01213719v1
|
|
Preface of Proceedings of the Workshop on OCL and Textual Modelling (OCL 2011)Electronic Communications of the EASST, 2011, OCL and Textual Modelling 2011, 44
Article dans une revue
hal-00647006v1
|
|
Semantics, Calculi, and Analysis for Object-Oriented SpecificationsActa Informatica, 2009, 46 (4), pp.255-284. ⟨10.1007/s00236-009-0093-8⟩
Article dans une revue
hal-01214519v1
|
|
Proving Fairness and Implementation Correctness of a Microkernel Scheduler.Journal of Automated Reasoning, 2009, In: G. Klein, R. Huuck and B. Schlich: Special Issue on Operating System Verification, 42 (2-4), pp.349-388. ⟨10.1007/s10817-009-9119-8⟩
Article dans une revue
hal-01214588v1
|
|
An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP++Journal of Automated Reasoning, 2008, 41 (3), pp.219-249. ⟨10.1007/s10817-008-9108-3⟩
Article dans une revue
hal-01214567v1
|
Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS), Jun 2023, Toulouse, France. pp.136-141, ⟨10.1109/ICECCS59891.2023.00025⟩
Communication dans un congrès
hal-04500099v1
|
|
|
|
On the Semantics of Polychronous Polytimed Specifications18th International Conference on Formal Modeling and Analysis of Timed Systems, Sep 2020, Vienna, Austria. pp.23-40, ⟨10.1007/978-3-030-57628-8_2⟩
Communication dans un congrès
hal-02931403v1
|
|
|
TESL: a Model with Metric Time for Modeling and Simulation27th International Symposium on Temporal Representation and Reasoning, Sep 2020, Bozen-Bolzano, Italy. ⟨10.4230/LIPIcs.TIME.2020.15⟩
Communication dans un congrès
hal-02931401v1
|
Using Ontologies in Formal Developments Targeting CertificationInternational Conference on Integrated Formal Methods (iFM 2019), Nov 2019, Bergen, Norway. pp.65-82, ⟨10.1007/978-3-030-34968-4_4⟩
Communication dans un congrès
hal-04500138v1
|
|
Isabelle/DOF: Design and ImplementationInternational Conference on Software Engineering and Formal Methods (SEFM 2019), Sep 2019, Oslo (Norway), Norway. pp.275-292, ⟨10.1007/978-3-030-30446-1_15⟩
Communication dans un congrès
hal-04500171v1
|
|
|
|
Making Agile Development Processes fit for V-style Certification Procedures9th European Congress on Embedded Real Time Software and Systems (ERTS 2018), Jan 2018, Toulouse, France
Communication dans un congrès
hal-01702815v1
|
|
|
Using the Isabelle Ontology Framework. Linking the Formal with the InformalInternational Conference on Intelligent Computer Mathematics (CICM), 2018, Hagenberg,, Austria. pp.23--38, ⟨10.1007/978-3-319-96812-4_3⟩
Communication dans un congrès
hal-01875734v1
|
|
|
A Symbolic Operational Semantics for TESL with an Application to Heterogeneous System Testing15th International Conference on Formal Modelling and Analysis of Timed Systems FORMATS 2017, Sep 2017, Berlin, Germany. ⟨10.1007/978-3-319-65765-3_18⟩
Communication dans un congrès
hal-01583815v1
|
Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of PathsInternational Conference on Interactive Theorem Proving ITP 2016, Aug 2016, Nancy, France
Communication dans un congrès
hal-01702847v1
|
|
Infeasible Paths Elimination by Symbolic Execution TechniquesInteractive Theorem Proving. ITP 2016, 2016, NANCY, France
Communication dans un congrès
hal-01632902v1
|
|
A Method for Pruning Infeasible Paths via Graph Transformations and Symbolic Execution2016 {IEEE} International Conference on Software Quality, Reliability and Security, {QRS} , Aug 2016, Vienna, Austria
Communication dans un congrès
hal-01655414v1
|
|
|
|
Recent Developments in OCL and Textual ModellingInternational Workshop on OCL and Textual Modeling (OCL 2016), Oct 2016, Saint-Malo, France. pp.157 - 165
Communication dans un congrès
hal-01589574v1
|
Monadic Sequence Testing and Explicit Test-RefinementsTests and Proofs - 10th International Conference, 2016, Vienna, France
Communication dans un congrès
hal-01765528v1
|
|
Formal API Specification of the PikeOS Separation KernelNASA Formal Methods - 7th International Symposium, NFM 2015,, Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi, Apr 2015, Pasadena, CA, USA, France. pp.375--389, ⟨10.1007/978-3-319-17524-9_26⟩
Communication dans un congrès
hal-01275405v1
|
|
|
|
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.515th International Workshop on OCL and Textual Modeling co-located with 18th International Conference on Model Driven Engineering Languages and Systems, Oct 2015, Karlsruhe, Germany. pp.199
Communication dans un congrès
hal-01213440v1
|
|
|
Towards a formal semantics of the TESL specification language3rd International Workshop on the Globalization Of Modeling Languages (GEMOC 2015), Benoit Combemale; Julien Deantoni; Jeff Gray, Sep 2015, Ottawa, Canada. pp.14-19
Communication dans un congrès
hal-01239669v1
|
Panel Discussion: Proposals for Improving OCLOCL 2014, Sep 2014, Valencia, Spain. pp.83-99
Communication dans un congrès
hal-01222939v1
|
|
Towards a Tool for Featherweight OCL: A Case Study On Semantic ReflectionProceedings of the 14th International Workshop on OCL and Textual Modelling co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Sep 2014, Valencia, Spain
Communication dans un congrès
hal-01214466v1
|
|
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving SystemsMKM/Calculemus/DML, Jul 2013, Bath, United Kingdom. pp.359-363
Communication dans un congrès
hal-00908980v1
|
|
On the Semantics of Object-Oriented Data Structures and Path ExpressionsProceedings of the MODELS 2013 OCL Workshop co-located with the 16th International ACM/IEEE Conference on Model Driven Engineering Languages and Systems (MODELS 2013), Sep 2013, Miami, United States
Communication dans un congrès
hal-01214460v1
|
|
|
|
The Circus Testing Theory Revisited in Isabelle/HOLFormal Methods and Software Engineering - 15th International Conference on Formal Engineering Method, ICFEM, Oct 2013, Queenstown, New Zealand. pp.131--147, ⟨10.1007/978-3-642-41202-8_10⟩
Communication dans un congrès
hal-01126803v1
|
Test Program Generation for a Microprocessor -- A Case-StudyProceedings of the 6th Intl. Conf. on Test and Proof (TAP '13), 2013, Budapest, France
Communication dans un congrès
hal-01765545v1
|
|
A Specification-Based Test Case Generation Method for UML/OCLModels in Software Engineering - Workshops and Symposia at MODELS 2010, Oct 2010, Oslo, Norway
Communication dans un congrès
hal-01760563v1
|
Symbolic Methods in Testing (Dagstuhl Seminar 13021)Thierry Jéron and Margus Veanes and Burkhart Wolff. Dagstuhl Publishing, 3 (1), pp.1-29, 2013, ⟨10.4230/DagRep.3.1.1⟩
Ouvrages
hal-00823739v1
|
|
Testing Software and SystemsSpringer, LNCS-7019, 2011, Lecture Notes in Computer Science, 978-3-642-24579-4. ⟨10.1007/978-3-642-24580-0⟩
Ouvrages
hal-01583913v1
|
Philosophers may Dine - Definitively!16th International Conference on Integrated Formal Methods, 2020, ⟨10.1007/978-3-030-63461-2_23⟩
Chapitre d'ouvrage
hal-03134972v1
|
|
The Circus Testing Theory Revisited in Isabelle/HOLLindsay Groves and Jing Sun. Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods(ICFEM), Springer-Verlag, 2013
Chapitre d'ouvrage
hal-00945960v1
|
The Unified Policy Framework (UPF)2014
Autre publication scientifique
hal-01765542v1
|
|
Formal Specification of a Generic Separation Kernel2013
Autre publication scientifique
hal-01765535v1
|
|
|
Using Isabelle/UTP for the Verification of Sorting Algorithms A Case Study2018
Pré-publication, Document de travail
hal-04504877v1
|
|
|
Modelling and Proving Safety in Autonomous Cars Scenarios in HOL-CSP[Research Report] 1, University Paris-Saclay; IRT SystemX, Palaiseau. 2021, pp.81
Rapport
hal-03429597v2
|
|
|
HOL-TestGen Version 1.8 USER GUIDE[Technical Report] Univeristé Paris-Saclay; LRI - CNRS, University Paris-Sud. 2016
Rapport
hal-01765526v1
|
|
|
Pruning Infeasible Paths via Graph Transformations and Symbolic Execution: a Method and a Tool[Research Report] 1588, Laboratoire de Recherche en Informatique [LRI], UMR 8623, Bâtiments 650-660, Université Paris-Sud, 91405 Orsay Cedex. 2016
Rapport
hal-01764525v1
|