![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Franck Cassez
Person information
Refine list
![note](https://dblp.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j17]Franck Cassez
, Joanne Fuller, Horacio Mijail Anton Quiles
:
Deductive verification of smart contracts with Dafny. Int. J. Softw. Tools Technol. Transf. 26(2): 131-145 (2024) - [c53]Franck Cassez:
Deductive Verification of Smart Contracts (Invited Talk). FMBC@CAV 2024: 1:1-1:1 - 2023
- [c52]Franck Cassez
, Joanne Fuller, Milad K. Ghale, David J. Pearce
, Horacio Mijail Anton Quiles:
Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. FM 2023: 571-583 - [i15]Franck Cassez, Joanne Fuller, Milad K. Ghale, David J. Pearce, Horacio Mijail Anton Quiles:
Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. CoRR abs/2303.00152 (2023) - 2022
- [c51]Franck Cassez
, Joanne Fuller, Horacio Mijail Anton Quiles:
Deductive Verification of Smart Contracts with Dafny. FMICS 2022: 50-66 - [c50]Franck Cassez
, Joanne Fuller, Aditya Asgaonkar:
Formal Verification of the Ethereum 2.0 Beacon Chain. TACAS (1) 2022: 167-182 - [i14]Franck Cassez, Joanne Fuller, Horacio Mijail Anton Quiles:
Deductive Verification of Smart Contracts with Dafny. CoRR abs/2208.02920 (2022) - 2021
- [j16]Franck Cassez, Peter Gjøl Jensen
, Kim Guldstrand Larsen
:
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction. Fundam. Informaticae 178(1-2): 31-57 (2021) - [c49]Franck Cassez
:
Verification of the Incremental Merkle Tree Algorithm with Dafny. FM 2021: 445-462 - [i13]Franck Cassez:
Verification of the Incremental Merkle Tree Algorithm with Dafny. CoRR abs/2105.06009 (2021) - [i12]Franck Cassez, Joanne Fuller, Aditya Asgaonkar:
Formal Verification of the Ethereum 2.0 Beacon Chain. CoRR abs/2110.12909 (2021) - 2020
- [i11]Franck Cassez, Peter Gjøl Jensen, Kim Guldstrand Larsen:
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction. CoRR abs/2007.10539 (2020)
2010 – 2019
- 2018
- [j15]Xi Zheng
, Christine Julien
, Rodion M. Podorozhny, Franck Cassez
, Thierry Rakotoarivelo:
Efficient and Scalable Runtime Monitoring for Cyber-Physical System. IEEE Syst. J. 12(2): 1667-1678 (2018) - 2017
- [j14]Xi Zheng
, Christine Julien
, Hongxu Chen, Rodion M. Podorozhny, Franck Cassez
:
Real-Time Simulation Support for Runtime Verification of Cyber-Physical Systems. ACM Trans. Embed. Comput. Syst. 16(4): 106:1-106:24 (2017) - [c48]Franck Cassez
, Pablo González de Aledo, Peter Gjøl Jensen
:
WUPPAAL: Computation of Worst-Case Execution-Time for Binary Programs with UPPAAL. Models, Algorithms, Logics and Tools 2017: 560-577 - [c47]Franck Cassez
, Peter Gjøl Jensen
, Kim Guldstrand Larsen
:
Refinement of Trace Abstraction for Real-Time Programs. RP 2017: 42-58 - [c46]Franck Cassez
, Anthony M. Sloane
:
ScalaSMT: satisfiability modulo theory in Scala (tool paper). SCALA@SPLASH 2017: 51-55 - [c45]Franck Cassez
, Anthony M. Sloane
, Matthew Roberts
, Matthew Pigram, Pongsak Suvanpong, Pablo González de Aledo Marugán:
Skink: Static Analysis of Programs in LLVM Intermediate Representation - (Competition Contribution). TACAS (2) 2017: 380-384 - 2016
- [j13]Franck Cassez
, Ron van der Meyden
, Chenyi Zhang
:
The complexity of synchronous notions of information flow security. Theor. Comput. Sci. 631: 16-42 (2016) - [c44]Anthony M. Sloane
, Franck Cassez
, Scott Buckley
:
The sbt-rats parser generator plugin for Scala (tool paper). SCALA@SPLASH 2016: 110-113 - 2015
- [j12]Gilles Benattar, Franck Cassez
, Didier Lime
, Olivier H. Roux:
Control and synthesis of non-interferent timed systems. Int. J. Control 88(2): 217-236 (2015) - [c43]Franck Cassez
, Frowin Ziegler:
Verification of Concurrent Programs Using Trace Abstraction Refinement. LPAR 2015: 233-248 - [c42]Xi Zheng
, Christine Julien
, Rodion M. Podorozhny, Franck Cassez
:
BraceAssertion: Runtime Verification of Cyber-Physical Systems. MASS 2015: 298-306 - [c41]Franck Cassez
, Takashi Matsuoka, Edward Pierzchalski, Nathan Smyth:
Perentie: Modular Trace Refinement and Selective Value Tracking - (Competition Contribution). TACAS 2015: 439-442 - [c40]Franck Cassez
, Pablo González de Aledo Marugán:
Timed Automata for Modelling Caches and Pipelines. MARS 2015: 37-45 - 2014
- [c39]Franck Cassez
, Christian Müller
, Karla Burnett:
Summary-Based Inter-Procedural Analysis via Modular Trace Refinement. FSTTCS 2014: 545-556 - [c38]Romain Brenguier, Franck Cassez
, Jean-François Raskin:
Energy and mean-payoff timed games. HSCC 2014: 283-292 - [e4]Franck Cassez
, Jean-François Raskin:
Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings. Lecture Notes in Computer Science 8837, Springer 2014, ISBN 978-3-319-11935-9 [contents] - [i10]Franck Cassez, Ron van der Meyden, Chenyi Zhang:
The Complexity of Synchronous Notions of Information Flow Security. CoRR abs/1402.0601 (2014) - 2013
- [j11]Béatrice Bérard, Franck Cassez
, Serge Haddad, Didier Lime
, Olivier H. Roux:
The expressive power of time Petri nets. Theor. Comput. Sci. 474: 1-20 (2013) - [c37]Franck Cassez
, Jean-Luc Béchennec:
Timing Analysis of Binary Programs with UPPAAL. ACSD 2013: 41-50 - [c36]Franck Cassez
, Alban Grastien:
Predictability of Event Occurrences in Timed Systems. FORMATS 2013: 62-76 - [c35]Sebastian Biallas, Mads Chr. Olesen, Franck Cassez
, Ralf Huuck:
PtrTracker: Pragmatic pointer analysis. SCAM 2013: 69-73 - [p2]Franck Cassez
, Nicolas Markey
:
Control of Timed Systems. Communicating Embedded Systems 2013: 67-105 - [p1]Franck Cassez
, Stavros Tripakis
:
Fault Diagnosis of Timed Systems. Communicating Embedded Systems 2013: 107-138 - [i9]Franck Cassez, Alban Grastien:
Predictability of Event Occurrences in Timed Systems. CoRR abs/1306.0662 (2013) - 2012
- [j10]Franck Cassez
, Jérémy Dubreil, Hervé Marchand:
Synthesis of opaque systems with static and dynamic masks. Formal Methods Syst. Des. 40(1): 88-115 (2012) - [j9]Franck Cassez
:
The Complexity of Codiagnosability for Discrete Event and Timed Systems. IEEE Trans. Autom. Control. 57(7): 1752-1764 (2012) - [c34]Peter E. Bulychev, Franck Cassez
, Alexandre David, Kim Guldstrand Larsen
, Jean-François Raskin, Pierre-Alain Reynier:
Controllers with Minimal Observation Power (Application to Timed Systems). ATVA 2012: 223-237 - [c33]Franck Cassez
, René Rydhof Hansen
, Mads Chr. Olesen
:
What is a Timing Anomaly?. WCET 2012: 1-12 - [c32]Mark Bradley, Franck Cassez
, Ansgar Fehnker
, Thomas Given-Wilson
, Ralf Huuck:
High Performance Static Analysis for Industry. TAPAS@SAS 2012: 3-14 - [e3]Franck Cassez, Ralf Huuck, Gerwin Klein, Bastian Schlich:
Proceedings Seventh Conference on Systems Software Verification, SSV 2012, Sydney, Australia, 28-30 November 2012. EPTCS 102, 2012 [contents] - [i8]Peter E. Bulychev, Franck Cassez, Alexandre David, Kim G. Larsen, Jean-François Raskin, Pierre-Alain Reynier:
Controllers with Minimal Observation Power (Application to Timed Systems). CoRR abs/1207.1276 (2012) - [i7]Gilles Benattar, Franck Cassez, Didier Lime, Olivier H. Roux:
Control and Synthesis of Non-Interferent Timed Systems. CoRR abs/1207.4984 (2012) - 2011
- [j8]Patricia Bouyer, Franck Cassez
, François Laroussinie:
Timed Modal Logics for Real-Time Systems - Specification, Verification and Control. J. Log. Lang. Inf. 20(2): 169-203 (2011) - [c31]Franck Cassez
:
Timed Games for Computing WCET for Pipelined Processors with Caches. ACSD 2011: 195-204 - [i6]Jean-Luc Béchennec, Franck Cassez:
Computation of WCET using Program Slicing and Real-Time Model-Checking. CoRR abs/1105.1633 (2011) - 2010
- [c30]Franck Cassez
:
The Complexity of Codiagnosability for Discrete Event and Timed Systems. ATVA 2010: 82-96 - [c29]Franck Cassez
:
Dynamic observers for fault diagnosis of timed systems. CDC 2010: 4359-4364 - [c28]Franck Cassez
, Ron van der Meyden
, Chenyi Zhang
:
The Complexity of Synchronous Notions of Information Flow Security. FoSSaCS 2010: 282-296 - [i5]Franck Cassez:
The Complexity of Codiagnosability for Discrete Event and Timed Systems. CoRR abs/1004.2550 (2010) - [i4]Franck Cassez:
A Note on Fault Diagnosis Algorithms. CoRR abs/1004.2764 (2010) - [i3]Franck Cassez, Stavros Tripakis:
Fault Diagnosis with Dynamic Observers. CoRR abs/1004.2810 (2010) - [i2]Franck Cassez:
Timed Games for Computing Worst-Case Execution-Times. CoRR abs/1006.1951 (2010) - [i1]Franck Cassez:
Dynamic Observers for Fault Diagnosis of Timed Systems. CoRR abs/1006.4681 (2010)
2000 – 2009
- 2009
- [c27]Franck Cassez
, Jérémy Dubreil, Hervé Marchand:
Dynamic Observers for the Synthesis of Opaque Systems. ATVA 2009: 352-367 - [c26]Franck Cassez
:
A note on fault diagnosis algorithms. CDC 2009: 6941-6946 - [c25]Gilles Benattar, Franck Cassez, Didier Lime, Olivier H. Roux:
Synthesis of Non-Interferent Timed Systems. FORMATS 2009: 28-42 - [c24]Franck Cassez
, Jan Jakob Jessen, Kim Guldstrand Larsen
, Jean-François Raskin, Pierre-Alain Reynier:
Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study. HSCC 2009: 90-104 - [c23]Franck Cassez
:
The Dark Side of Timed Opacity. ISA 2009: 21-30 - 2008
- [j7]Franck Cassez, Stavros Tripakis:
Fault Diagnosis with Static and Dynamic Observers. Fundam. Informaticae 88(4): 497-540 (2008) - [j6]Béatrice Bérard, Franck Cassez
, Serge Haddad, Didier Lime
, Olivier H. Roux:
When are Timed Automata weakly timed bisimilar to Time Petri Nets? Theor. Comput. Sci. 403(2-3): 202-220 (2008) - [e2]Franck Cassez, Claude Jard:
Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008. Proceedings. Lecture Notes in Computer Science 5215, Springer 2008, ISBN 978-3-540-85777-8 [contents] - 2007
- [b1]Franck Cassez:
Control of Timed Systems. Institut de Recherche en Communications et Cybernétique de Nantes, France, 2007 - [c22]Franck Cassez, Stavros Tripakis, Karine Altisen:
Sensor Minimization Problems with Static or Dynamic Observers for Fault Diagnosis. ACSD 2007: 90-99 - [c21]Franck Cassez
, Alexandre David, Kim Guldstrand Larsen, Didier Lime, Jean-François Raskin
:
Timed Control with Observation Based and Stuttering Invariant Strategies. ATVA 2007: 192-206 - [c20]Franck Cassez
:
Efficient On-the-Fly Algorithms for Partially Observable Timed Games. FORMATS 2007: 5-24 - [c19]Franck Cassez
, Stavros Tripakis
, Karine Altisen:
Synthesis Of Optimal-Cost Dynamic Observers for Fault Diagnosis of Discrete-Event Systems. TASE 2007: 316-325 - 2006
- [j5]Franck Cassez
, Olivier H. Roux:
Structural translation from Time Petri Nets to Timed Automata. J. Syst. Softw. 79(10): 1456-1468 (2006) - [c18]Karine Altisen, Franck Cassez
, Stavros Tripakis
:
Monitoring and fault-diagnosis with digital clocks. ACSD 2006: 101-110 - [c17]Franck Cassez, Thomas Chatain, Claude Jard:
Symbolic Unfoldings for Networks of Timed Automata. ATVA 2006: 307-321 - 2005
- [c16]Béatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, Olivier H. Roux:
Comparison of Different Semantics for Time Petri Nets. ATVA 2005: 293-307 - [c15]Franck Cassez, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen
, Didier Lime:
Efficient On-the-Fly Algorithms for the Analysis of Timed Games. CONCUR 2005: 66-80 - [c14]Patricia Bouyer, Franck Cassez, François Laroussinie:
Modal Logics for Timed Control. CONCUR 2005: 81-94 - [c13]Béatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, Olivier H. Roux:
Comparison of the Expressiveness of Timed Automata and Time Petri Nets. FORMATS 2005: 211-225 - [c12]Béatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, Olivier H. Roux:
When Are Timed Automata Weakly Timed Bisimilar to Time Petri Nets? FSTTCS 2005: 273-284 - 2004
- [j4]Franck Cassez, Claire Pagetti, Olivier H. Roux:
A Timed Extension for ALTARICA. Fundam. Informaticae 62(3-4): 291-332 (2004) - [c11]Patricia Bouyer, Franck Cassez, Emmanuel Fleury, Kim Guldstrand Larsen:
Optimal Strategies in Priced Timed Game Automata. FSTTCS 2004: 148-160 - [c10]Patricia Bouyer, Franck Cassez
, Emmanuel Fleury, Kim Guldstrand Larsen:
Synthesis of Optimal Strategies Using HyTech. GDV@CAV 2004: 11-31 - [c9]Franck Cassez
, Olivier H. Roux:
Structural Translation from Time Petri Nets to Timed Automata. AVoCS 2004: 145-160 - 2003
- [c8]Gilles Bernot, Franck Cassez
, Jean-Paul Comet, Franck Delaplace, Céline Müller, Olivier F. Roux:
Semantics of Biological Regulatory Networks. BioConcur@CONCUR 2003: 3-14 - 2002
- [c7]Franck Cassez
, Thomas A. Henzinger, Jean-François Raskin:
A Comparison of Control Problems for Timed and Hybrid Systems. HSCC 2002: 134-148 - [c6]Frédéric Herbreteau, Franck Cassez, Alain Finkel, Olivier F. Roux, Grégoire Sutre:
Verification of Embedded Reactive Fiffo Systems. LATIN 2002: 400-414 - [c5]Armelle Prigent, Franck Cassez, Philippe Dhaussy, Olivier F. Roux:
Extending the Translation from SDL to Promela. SPIN 2002: 79-94 - 2001
- [j3]Frédéric Herbreteau, Franck Cassez
, Olivier F. Roux:
Application of Partial-Order Methods to Reactive Programs with Event Memorization. Real Time Syst. 20(3): 287-316 (2001) - [e1]Franck Cassez, Claude Jard, Brigitte Rozoy, Mark Dermot Ryan:
Modeling and Verification of Parallel Processes, 4th Summer School, MOVEP 2000, Nantes, France, June 19-23, 2000. Lecture Notes in Computer Science 2067, Springer 2001, ISBN 3-540-42787-2 [contents] - 2000
- [c4]Franck Cassez, François Laroussinie:
Model-Checking for Hybrid Systems by Quotienting and Constraints Solving. CAV 2000: 373-388 - [c3]Franck Cassez, Kim Guldstrand Larsen:
The Impressive Power of Stopwatches. CONCUR 2000: 138-152 - [c2]Franck Cassez, Mark Dermot Ryan, Pierre-Yves Schobbens
:
Proving feature non-interaction with Alternating-Time Temporal Logic. FIREworks 2000: 85-103
1990 – 1999
- 1999
- [j2]Olivier F. Roux, Vlad Rusu, Franck Cassez
:
Hybrid Verifications of Reactive Programs. Formal Aspects Comput. 11(4): 448-471 (1999) - 1998
- [c1]Grégoire Sutre, Alain Finkel, Olivier F. Roux, Franck Cassez
:
Effective Recognizability and Model Checking of Reactive Fiffo Automata. AMAST 1998: 106-123 - 1995
- [j1]Franck Cassez
, Olivier F. Roux:
Compilation of the ELECTRE Reactive Language into Finite Transition Systems. Theor. Comput. Sci. 146(1&2): 109-143 (1995)
Coauthor Index
aka: Kim Guldstrand Larsen
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-05-23 22:13 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint