| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Zhengfeng Yang, Chao Huang 0015, Xin Chen 0027, Wang Lin, Zhiming Liu 0001 |
A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems.  |
FM  |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Aleksandar S. Dimovski, Claus Brabrand, Andrzej Wasowski |
Finding Suitable Variability Abstractions for Family-Based Analysis. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Adel Djoudi, Sébastien Bardin, Éric Goubault |
Recovering High-Level Conditions from Binary Programs. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Antonio Flores-Montoya |
Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Han Liu 0010, Yu Jiang 0001, Huafeng Zhang, Ming Gu 0001, Jiaguang Sun 0001 |
Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Stanislav Böhm, Ondrej Meca, Petr Jancar |
State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Yu Jiang 0001, Han Liu 0010, Houbing Song, Hui Kong 0004, Ming Gu 0001, Jiaguang Sun 0001, Lui Sha |
Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Gudmund Grov, Yuhui Lin, Vytautas Tumas |
Mechanised Verification Patterns for Dafny. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, César Kunz, Keiko Nakata 0001, Jorge Luis Sacchini, Hendrik Tews, Thomas Tuerk |
Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Ori Lahav 0001, Viktor Vafeiadis |
Explaining Relaxed Memory Models with Program Transformations. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng, Harald Ruess |
Compositional Parameter Synthesis. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep |
Counter-Example Guided Program Verification. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Li Li 0044, Jun Sun 0001, Jin Song Dong |
Automated Verification of Timed Security Protocols with Clock Drift. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Saksham Chand, Yanhong A. Liu, Scott D. Stoller |
Formal Verification of Multi-Paxos for Distributed Consensus. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan |
Validated Simulation-Based Verification of Delayed Differential Dynamics. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Ofer Strichman, Maor Veitsman |
Regression Verification for Unbalanced Recursive Functions. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Amirhossein Vakili, Nancy A. Day |
Finite Model Finding Using the Logic of Equality with Uninterpreted Functions. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Bjørnar Luteberget, Christian Johansen, Claus Feyling, Martin Steffen |
Rule-Based Incremental Verification Tools Applied to Railway Designs and Regulations. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Letan, Pierre Chifflier, Guillaume Hiet, Pierre Néron, Benjamin Morin |
SpecCert: Specifying and Verifying Hardware-Based Security Enforcement. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Victor B. F. Gomes, Georg Struth |
Modal Kleene Algebra Applied to Program Correctness. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Yusuke Kawamoto 0001, Fabrizio Biondi, Axel Legay |
Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Miran Hasanagic, Peter W. V. Tran-Jørgensen, Kenneth Lausdahl, Peter Gorm Larsen |
Formalising and Validating the Interface Description in the FMI Standard. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Heinrich Ody, Martin Fränzle, Michael R. Hansen |
Discounted Duration Calculus. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan Peleska 0001, Wen-ling Huang |
Industrial-Strength Model-Based Testing of Safety-Critical Systems. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Cavada, Alessandro Cimatti, Luigi Crema, Mattia Roccabruna, Stefano Tonetta |
Model-Based Design of an Energy-System Embedded Controller Using Taste. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Georgios Giantamidis, Stavros Tripakis |
Learning Moore Machines from Input-Output Traces. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, Anna Philippou (eds.) |
FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Mahieddine Dellabani, Jacques Combaz, Marius Bozga, Saddek Bensalem |
Local Planning of Multiparty Interactions with Bounded Horizons. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Anton Wijs, Thomas Neele, Dragan Bosnacki |
GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, Wei-Ngan Chin |
Automated Mutual Explicit Induction Proof in Separation Logic. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Morten Bisgaard, David Gerhardt, Holger Hermanns, Jan Krcál, Gilles Nies, Marvin Stenger |
Battery-Aware Scheduling in Low Orbit: The GomX-3 Case. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter H. Schmitt, Mattias Ulbrich |
Axiomatization of Typed First-Order Logic. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Bharti Chimdyalwar, Priyanka Darke, Anooj Chavda, Sagar Vaghani, Avriti Chauhan |
Eliminating Static Analysis False Positives Using Loop Abstraction and Bounded Model Checking. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamaric, Ganesh Gopalakrishnan |
Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Tao Liu, Ralf Huuck |
Case Study: Static Security Analysis of the Android Goldfish Kernel. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Guillaume Brat, David H. Bushnell, Misty D. Davies, Dimitra Giannakopoulou, Falk Howar, Temesghen Kahsai |
Verifying the Safety of a Flight-Critical System. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Elvira Albert, Puri Arenas, Jesús Correas, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, Germán Puebla, Guillermo Román-Díez |
Resource Analysis: From Sequential to Concurrent and Distributed Programs. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Jiang Liu 0009, Naijun Zhan, Hengjun Zhao, Liang Zou |
Abstraction of Elementary Hybrid Systems by Variable Transformation. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Eisentraut, Jens Chr. Godskesen, Holger Hermanns, Lei Song 0001, Lijun Zhang 0001 |
Probabilistic Bisimulation for Realistic Schedulers. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew Sogokon, Paul B. Jackson |
Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Hamid Bagheri, Eunsuk Kang, Sam Malek, Daniel Jackson 0001 |
Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Li Li 0044, Jun Sun 0001, Yang Liu 0003, Jin Song Dong |
Verifying Parameterized Timed Security Protocols. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor, Wei-Ngan Chin |
Certified Reasoning with Infinity. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Søren Debois, Thomas T. Hildebrandt, Tijs Slaats |
Safety, Liveness and Run-Time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Matt Lewis, Georg Weissenbacher |
Proving Safety with Trace Automata and Bounded Model Checking. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Saurabh Joshi 0001, Daniel Kroening |
Property-Driven Fence Insertion Using Reorder Bounded Model Checking. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthew Fernandez, June Andronick, Gerwin Klein, Ihor Kuz |
Automated Verification of RPC Stub Code. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Neil Evans |
Software Development and Authentication for Arms Control Information Barriers. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Xueyang Zhu, Rongjie Yan, Yu-Lei Gu, Jian Zhang 0001, Wenhui Zhang, Guangquan Zhang 0002 |
Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Wolfgang Ahrendt, Jesús Mauricio Chimento, Gordon J. Pace, Gerardo Schneider |
A Specification Language for Static and Runtime Verification of Data and Control Properties. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Nadia Polikarpova, Julian Tschannen, Carlo A. Furia |
A Fully Verified Container Library. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Cornelius Diekmann, Lars Hupel, Georg Carle |
Semantics-Preserving Simplification of Real-World Firewall Rule Sets. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Shin Nakajima 0001 |
Using Real-Time Maude to Model Check Energy Consumption Behavior. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Lecomte |
Formal Virtual Modelling and Data Verification for Supervision Systems. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Musab A. AlTurki, Omar Alzuhaibi |
Towards Formal Verification of Orchestration Computations Using the 핂 Framework. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Sylvain Conchon, Alain Mebsout, Fatiha Zaïdi |
Certificates for Parameterized Model Checking. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Yuan Feng 0001, Ernst Moritz Hahn, Andrea Turrini, Lijun Zhang 0001 |
QPMC: A Model Checker for Quantum Programs and Protocols. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Bruno Miranda, Henrique Masini, Rodrigo Reis |
Using Simulink Design Verifier for Automatic Generation of Requirements-Based Tests. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham |
Automated Circular Assume-Guarantee Reasoning. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Nikolaj S. Bjørner, Frank S. de Boer (eds.) |
FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | David Schneider 0001, Michael Leuschel, Tobias Witt |
Model-Based Problem Solving for University Timetable Validation and Improvement. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Werner Damm |
AVACS: Automatic Verification and Analysis of Complex Systems Highlights and Lessons Learned. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | John Derrick, Graeme Smith 0001 |
A Framework for Correctness Criteria on Weak Memory Models. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Xiaoning Du 0001, Yang Liu 0003, Alwen Tiu |
Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Hauck-Stattelmann, Sebastian Biallas, Bastian Schlich, Stefan Kowalewski, Raoul Jetley |
Analyzing the Restart Behavior of Industrial Control Applications. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | William Durand, Sébastien Salva |
Autofunk: An Inference-Based Formal Model Generation Framework for Production Systems. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Tim Quatmann, Nils Jansen 0001, Christian Dehnert, Ralf Wimmer 0001, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker 0001 |
Counterexamples for Expected Rewards. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Thao Dang 0001, Tommaso Dreossi, Carla Piazza |
Parameter Synthesis Through Temporal Logic Specifications. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Tim Nelson, Andrew D. Ferguson, Shriram Krishnamurthi |
Static Differential Program Analysis for Software-Defined Networks. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Gianluca Amato, Simone Di Nardo Di Maio, Maria Chiara Meo, Francesca Scozzari |
Narrowing Operators on Template Abstract Domains. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Mathijs Schuts, Jozef Hooman |
Formalizing the Concept Phase of Product Development. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim |
Verifying Opacity of a Transactional Mutex Lock. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Taro Kurita, Fuyuki Ishikawa, Keijiro Araki |
Practices for Formal Models as Documents: Evolution of VDM Application to "Mobile FeliCa" IC Chip Firmware. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Aliakbar Safilian, Tom Maibaum, Zinovy Diskin |
The Semantics of Cardinality-Based Feature Models via Formal Languages. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Julien Bringer, Hervé Chabanne, Daniel Le Métayer, Roch Lescuyer |
Privacy by Design in Practice: Reasoning about Privacy Properties of Biometric System Architectures. |
FM |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre Roux, Pierre-Loïc Garoche |
Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Piotr Kordy, Rom Langerak, Sjouke Mauw, Jan Willem Polderman |
A Symbolic Algorithm for the Analysis of Robust Timed Automata. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Aarti Gupta, V. M. Achutha KiranKumar, Rajnish Ghughal |
Formally Verifying Graphics FPU - An Intel® Experience. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Alasdair Armstrong, Victor B. F. Gomes, Georg Struth |
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Mitsch, Jan-David Quesel, André Platzer |
Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid Systems. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Parasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh Viswanathan 0001, César A. Muñoz |
Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Kyungmin Bae, Peter Csaba Ölveczky, José Meseguer 0001 |
Definition, Semantics, and Analysis of Multirate Synchronous AADL. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Yuan Feng 0001, Lijun Zhang 0001 |
When Equivalence and Bisimulation Join Forces in Probabilistic Automata. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Yan Liu 0012, Lin Gui 0002, Yang Liu 0003 |
MDP-Based Reliability Analysis of an Ambient Assisted Living System. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Leo Freitas, Iain Whiteside |
Proof Patterns for Formal Methods. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | K. Vasanta Lakshmi, Aravind Acharya, Raghavan Komondoor |
Checking Liveness Properties of Presburger Counter Systems Using Reachability Analysis. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Pedro R. G. Antonino, Augusto Sampaio, Jim Woodcock 0001 |
A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Guangdong Bai, Jianan Hao, Jianliang Wu, Yang Liu 0003, Zhenkai Liang, Andrew P. Martin |
TrustFound: Towards a Formal Foundation for Model Checking Trusted Computing Platforms. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Vojtech Forejt, Daniel Kroening, Ganesh Narayanaswamy, Subodh Sharma 0001 |
Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jim Woodcock 0001 |
Engineering UToPiA - Formal Semantics for CML. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Ian J. Hayes, Larissa Meinicke |
Invariants, Well-Founded Statements and Real-Time Program Algebra. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Suman Roy 0001, A. S. M. Sajeev, Srivibha Sripathy |
Diagnosing Industrial Business Processes: Early Experiences. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Scheben, Peter H. Schmitt |
Efficient Self-composition for Weakest Precondition Calculi. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | H.-Christian Estler, Carlo A. Furia, Martin Nordio, Marco Piccioni, Bertrand Meyer 0001 |
Contracts in Practice. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Chris Marriott, Ana Cavalcanti 0001 |
SCJ: Memory-Safety Checking without Annotations. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | K. Rustan M. Leino, Michal Moskal |
Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim |
Quiescent Consistency: Defining and Verifying Relaxed Linearizability. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Frank Zeyda, Thiago L. V. L. Santos, Ana Cavalcanti 0001, Augusto Sampaio |
A Modular Theory of Object Orientation in Higher-Order UTP. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Roland Wen, Annabelle McIver, Carroll Morgan |
Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Maria Christakis, K. Rustan M. Leino, Wolfram Schulte |
Formalizing and Verifying a Modern Build Language. |
FM |
2014 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license