Search results for "isabelle"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
16	Filip Maric	Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL.	Theor. Comput. Sci.	2010	DBLP DOI BibTeX RDF
16	Florian Rabe 0001	Representing Isabelle in LF	LFMTP	2010	DBLP DOI BibTeX RDF
16	Jacques D. Fleuriot	Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL.	Automated Deduction in Geometry	2010	DBLP DOI BibTeX RDF
16	Petros Papapanagiotou, Jacques D. Fleuriot	An Isabelle-Like Procedural Mode for HOL Light.	LPAR (Yogyakarta)	2010	DBLP DOI BibTeX RDF
16	Jasmin Christian Blanchette	Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod.	LPAR short papers(Yogyakarta)	2010	DBLP DOI BibTeX RDF
16	Johannes Hölzl	Quantitative Information Flow Analysis in Isabelle.	AlgoSyn	2010	DBLP BibTeX RDF
16	Andrei Popescu 0001, Elsa L. Gunter	Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization.	FoSSaCS	2010	DBLP DOI BibTeX RDF
16	Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff	Unifying Theories in Isabelle/HOL.	UTP	2010	DBLP DOI BibTeX RDF
16	Amy P. Felty	Hybrid: Reasoning with Higher-Order Abstract Syntax in Coq and Isabelle.	MSFP@ICFP	2010	DBLP DOI BibTeX RDF
16	Laura I. Meikle, Jacques D. Fleuriot	Automation for Geometry in Isabelle/HOL.	PAAR@IJCAR	2010	DBLP DOI BibTeX RDF
16	Brian Huffman, Christian Urban	A New Foundation for Nominal Isabelle.	ITP	2010	DBLP DOI BibTeX RDF
16	Peter Lammich, Andreas Lochbihler	The Isabelle Collections Framework.	ITP	2010	DBLP DOI BibTeX RDF
16	Douglas J. Howe	Higher-Order Abstract Syntax in Isabelle/HOL.	ITP	2010	DBLP DOI BibTeX RDF
16	Florian Kammüller, Alexander Rein, Mark-Oliver Reiser	Feature link propagation across variability representations with Isabelle/HOL.	PLEASE@ICSE	2010	DBLP DOI BibTeX RDF
16	Maksym Bortin, Christoph Lüth	Structured Formal Development with Quotient Types in Isabelle/HOL.	AISC/MKM/Calculemus	2010	DBLP DOI BibTeX RDF
16	Serguei A. Mokhov, Joey Paquet	Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle	CoRR	2009	DBLP BibTeX RDF
16	Francisco Javier López-Fraguas, Stephan Merz, Juan Rodríguez-Hortalá	A Formalization of the Semantics of Functional-Logic Programming in Isabelle	CoRR	2009	DBLP BibTeX RDF
16	Armin Heller	A Fast SAT Solver for Isabelle in Standard ML.	Arch. Formal Proofs	2009	DBLP BibTeX RDF
16	Bart Kastermans	An Example of a Cofinitary Group in Isabelle/HOL.	Arch. Formal Proofs	2009	DBLP BibTeX RDF
16	Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu 0001	Theory support for weak higher order abstract syntax in Isabelle/HOL.	LFMTP	2009	DBLP DOI BibTeX RDF
16	Christian Doczkal, Jan Schwinghammer	Formalizing a strong normalization proof for Moggi's computational metalanguage: a case study in Isabelle/HOL-nominal.	LFMTP	2009	DBLP DOI BibTeX RDF
16	Carsten Varming, Lars Birkedal	Higher-Order Separation Logic in Isabelle/HOLCF.	MFPS	2008	DBLP DOI BibTeX RDF
16	Amine Chaieb	Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF
16	Jeremy E. Dawson	Isabelle Theories for Machine Words.	AVoCS	2007	DBLP DOI BibTeX RDF
16	Jesper Bengtson, Joachim Parrow	A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle.	SOS@LICS/ICALP	2007	DBLP DOI BibTeX RDF
16	Julien Narboux, Christian Urban	Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking.	LFMTP@CADE	2007	DBLP DOI BibTeX RDF
16	Lukas Bulwahn, Alexander Krauss 0001, Tobias Nipkow	Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL.	TPHOLs	2007	DBLP DOI BibTeX RDF
16	Jia Meng, Lawrence C. Paulson, Gerwin Klein	A Termination Checker for Isabelle Hoare Logic.	VERIFY	2007	DBLP BibTeX RDF
16	Lars Gesellensetter, Sabine Glesner, Elke Salecker	Formal Verification with Isabelle/HOL in Practice: Finding a Bug in the GCC Scheduler.	FMICS	2007	DBLP DOI BibTeX RDF
16	Maria Spichkova	Specification and seamless verification of embedded real-time systems: FOCUS on Isabelle. (PDF / PS)		2007	RDF
16	Frédéric Blanqui	An Isabelle formalization of protocol-independent secrecy with an application to e-commerce	CoRR	2006	DBLP BibTeX RDF
16	Tom Ridge	Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL	CoRR	2006	DBLP BibTeX RDF
16	Maksym Bortin, Einar Broch Johnsen, Christoph Lüth	Structured Formal Development in Isabelle.	Nord. J. Comput.	2006	DBLP BibTeX RDF
16	J. Nathan Foster, Dimitrios Vytiniotis	A Theory of Featherweight Java in Isabelle/HOL.	Arch. Formal Proofs	2006	DBLP BibTeX RDF
16	Lucas Dixon	A proof planning framework for Isabelle.		2006	RDF
16	Norbert Schirmer	Verification of sequential imperative programs in Isabelle-HOL.		2006	RDF
16	Jan Olaf Blech, Sabine Glesner, Johannes Leitner, Steffen Mülling	Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL.	COCV@ETAPS	2005	DBLP DOI BibTeX RDF
16	Martin Holub	: Review: Natural Language Processing for Online Applications: Text Retrieval, Extraction and Categorization, by Peter Jackson and Isabelle Moulinier.	Prague Bull. Math. Linguistics	2005	DBLP BibTeX RDF
16	Matthias Daum 0001, Stefan Maus, Norbert Schirmer, Mohamed Nassim Seghir	Integration of a Software Model Checker into Isabelle.	LPAR	2005	DBLP DOI BibTeX RDF
16	Steven Obua	Proving Bounds for Real Linear Programs in Isabelle/HOL.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
16	Michael Compton	Stenning's Protocol Implemented in UDP and Verified in Isabelle.	CATS	2005	DBLP BibTeX RDF
16	Tjark Weber	Bounded Model Generation for Isabelle/HOL.	D/PDPAR@IJCAR	2004	DBLP DOI BibTeX RDF
16	Norbert Schirmer	Analysing the Java package/access concepts in Isabelle/HOL.	Concurr. Pract. Exp.	2004	DBLP DOI BibTeX RDF
16	John Longley, Randy Pollack	Reasoning About CBV Functional Programs in Isabelle/HOL.	TPHOLs	2004	DBLP DOI BibTeX RDF
16	Jan Olaf Blech, Sabine Glesner	A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL.	GI Jahrestagung (2)	2004	DBLP BibTeX RDF
16	Nicole Rauch, Burkhart Wolff	Formalizing Java's Two's-Complement Integral Type in Isabelle/HOL.	FMICS	2003	DBLP DOI BibTeX RDF
16	Lawrence C. Paulson	The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf.	LMS J. Comput. Math.	2003	DBLP DOI BibTeX RDF
16	Christine Röckl, Daniel Hirschkoff	A fully adequate shallow embedding of the [pi]-calculus in Isabelle/HOL with mechanized syntax analysis.	J. Funct. Program.	2003	DBLP DOI BibTeX RDF
16	Laura Menini	Non-linear control for underactuated mechanical systems: Isabelle Fantoni and Rogelio Lozano; Springer, London, 2002, ISBN 1-85233-423-1.	Autom.	2002	DBLP DOI BibTeX RDF
16	Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel 0001	Isabelle/HOL - A Proof Assistant for Higher-Order Logic		2002	DOI RDF
16	Markus Wenzel 0001	Isabelle, Isar - a versatile environment for human readable formal proof documents. (PDF / PS)		2002	RDF
16	Leonor Prensa Nieto	Verification of parallel programs with the Owicki-Gries and Rely-Guarantee methods in Isabelle, HOL.		2002	RDF
16	David von Oheimb	Hoare logic for Java in Isabelle/HOL.	Concurr. Comput. Pract. Exp.	2001	DBLP DOI BibTeX RDF
16	Christine Röckl	A First-Order Syntax for the Pi-Calculus in Isabelle/HOL using Permutations.	MERLIN	2001	DBLP DOI BibTeX RDF
16	Jeremy E. Dawson, Rajeev Goré	Embedding Display Calculi into Logical Frameworks: Comparing Twelf and Isabelle.	CATS	2001	DBLP DOI BibTeX RDF
16	Marieke Huisman	Reasoning about Java programs in higher order logic using PVS and Isabelle.		2001	RDF
16	Yasuhiko Minamide, Koji Okuma	Verifying the CPS Transformation in Isabelle/HOL.	APLAS	2001	DBLP BibTeX RDF
16	David von Oheimb	Analyzing Java in Isabelle-HOL: formalization, type safety and Hoare logic. (PDF / PS)		2001	RDF
16	Christine Röckl	Proving Write Invalidate Cache Coherence with Bisimulations in Isabelle/HOL.	FBT	2000	DBLP BibTeX RDF
16	Lawrence C. Paulson	A Generic Tableau Prover and its Integration with Isabelle.	J. Univers. Comput. Sci.	1999	DBLP DOI BibTeX RDF
16	Christopher Kuner	Signaturgesetze und "Political Correctness" - Isabelle Couvert-Castéra: Wunder "à la francaise".	Datenschutz und Datensicherheit	1999	DBLP BibTeX RDF
16	David A. Basin, Stefan Friedrich 0001	Modeling a Hardware Synthesis Methodology in Isabelle.	Formal Methods Syst. Des.	1999	DBLP DOI BibTeX RDF
16	Wolfgang Naraschewski, Tobias Nipkow	Type Inference Verified: Algorithm W in Isabelle/HOL.	J. Autom. Reason.	1999	DBLP DOI BibTeX RDF
16	Tobias Nipkow, Leonor Prensa Nieto	Owicki/Gries in Isabelle/HOL.	FASE	1999	DBLP DOI BibTeX RDF
16	Dina Taiwé Kolyang	HOL-Z, an integrated formal support environment for Z in Isabelle/HOL.		1999	RDF
16	Florian Kammüller	Modular reasoning in Isabelle		1999	RDF
16	Sten Agerholm, Jacob Frost	Supporting Proof in VDM-SL using Isabelle.	Proof in VDM	1998	DBLP DOI BibTeX RDF
16	Steffen Helke, Thomas Neustupny, Thomas Santen	Automating Test Case Generation from Z Specifications with Isabelle.	ZUM	1997	DBLP DOI BibTeX RDF
16	David A. Basin, Stefan Friedrich 0001	Modeling a Hardware Synthesis Methodology in Isabelle.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	Kolyang 0001, Thomas Santen, Burkhart Wolff	A Structure Preserving Encoding of Z in Isabelle/HOL.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	Wolfgang Naraschewski, Tobias Nipkow	Type Inference Verified: Algorithm W in Isabelle/HOL.	TYPES	1996	DBLP DOI BibTeX RDF
16	Ina Kraan, Peter Baumann	Implementing Z in Isabelle.	ZUM	1995	DBLP DOI BibTeX RDF
16	Philippe de Groote	Linear Logic with Isabelle: Pruning the Proof Search Tree.	TABLEAUX	1995	DBLP DOI BibTeX RDF
16	Clemens Ballarin, Karsten Homann, Jacques Calmet	Theorems and Algorithms: An Interface between Isabelle and Maple.	ISSAC	1995	DBLP DOI BibTeX RDF	Maple
16	Lawrence C. Paulson	Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow)		1994	DOI RDF
16	David A. Basin	IsaWhelk Interpreted in Isabelle.	ICLP	1994	DBLP BibTeX RDF
16	Tobias Nipkow, Konrad Slind	I/Q Automata in Isabelle/HOL.	TYPES	1994	DBLP DOI BibTeX RDF
16	Lawrence C. Paulson	Isabelle: The Next 700 Theorem Provers	CoRR	1993	DBLP BibTeX RDF
16	Lawrence C. Paulson	A Formulation of the Simple Theory of Types (for Isabelle)	CoRR	1993	DBLP BibTeX RDF
16	P. A. J. Noel	Experimenting with Isabelle in ZF Set Theory.	J. Autom. Reason.	1993	DBLP DOI BibTeX RDF
16	Sara Kalvala	Using Isabelle to Prove Simple Theorems.	HUG	1993	DBLP DOI BibTeX RDF
16	Tobias Nipkow	Equational Reasoning in Isabelle.	Sci. Comput. Program.	1989	DBLP DOI BibTeX RDF
16	Tobias Nipkow	Term Rewriting and Beyond - Theorem Proving in Isabelle.	Formal Aspects Comput.	1989	DBLP DOI BibTeX RDF
16	Lawrence C. Paulson	Isabelle: The Next Seven Hundred Theorem Provers.	CADE	1988	DBLP DOI BibTeX RDF
14	Odette Mwilu Sangupamba, Nicolas Prat, Isabelle Comyn-Wattiau	A Taxonomy Development Method to Define the Vocabulary for Rule-Based Guidance in Complex Emerging Technologies.	Bus. Inf. Syst. Eng.	2024	DBLP DOI BibTeX RDF
14	Francesco Amato, Julien Jacques, Isabelle Prim-Allaz	Clustering longitudinal ordinal data via finite mixture of matrix-variate distributions.	Stat. Comput.	2024	DBLP DOI BibTeX RDF
14	Lucrezia Tosato, Victor Fortier, Isabelle Bloch, Catherine Pelachaud	Exploiting temporal information to detect conversational groups in videos and predict the next speaker.	Pattern Recognit. Lett.	2024	DBLP DOI BibTeX RDF
14	Carole H. Sudre, Kimberlin M. H. van Wijnen, Florian Dubost, Hieab Adams, David Atkinson, Frederik Barkhof, Mahlet A. Birhanu, Esther E. Bron, Robin Camarasa, Nish Chaturvedi, Yuan Chen, Zihao Chen, Shuai Chen, Qi Dou 0001, Tavia E. Evans, Ivan Ezhov, Haojun Gao, Marta Gironés-Sangüesa, Juan Domingo Gispert, Beatriz Gomez Anson, Alun D. Hughes, Mohammad Arfan Ikram, Silvia Ingala, Hans Rolf Jäger, Florian Kofler, Hugo J. Kuijf, Denis Kutnar, Minho Lee, Bo Li 0088, Luigi Lorenzini, Bjoern H. Menze, José Luis Molinuevo, Yiwei Pan, Élodie Puybareau, Rafael Rehwald, Ruisheng Su, Pengcheng Shi, Lorna Smith, Therese Tillin, Guillaume Tochon, Hélène Urien, Bas H. M. van der Velden, Isabelle F. van der Velpen, Benedikt Wiestler, Frank J. Wolters, Pinar Yilmaz, Marius de Groot, Meike W. Vernooij, Marleen de Bruijne	Where is VALDO? VAscular Lesions Detection and segmentatiOn challenge at MICCAI 2021.	Medical Image Anal.	2024	DBLP DOI BibTeX RDF
14	Zuyi Yu, Amar Kachenoura, Régine Le Bouquin-Jeannès, Huazhong Shu, Paul Berraute, Anca Nica, Isabelle Merlet, Laurent Albera, Ahmad Karfoul	Electrophysiological brain imaging based on simulation-driven deep learning in the context of epilepsy.	NeuroImage	2024	DBLP DOI BibTeX RDF
14	Nasir Wabe, Isabelle Meulenbroeks, Guogui Huang, Sandun Malpriya Silva, Leonard C. Gray, Jacqueline C. T. Close, Stephen Lord, Johanna I. Westbrook	Development and internal validation of a dynamic fall risk prediction and monitoring tool in aged care using routinely collected electronic health data: a landmarking approach.	J. Am. Medical Informatics Assoc.	2024	DBLP DOI BibTeX RDF
14	Isabelle Hupont, David Fernández Llorca, Sandra Baldassarri, Emilia Gómez	Use case cards: a use case reporting framework inspired by the European AI Act.	Ethics Inf. Technol.	2024	DBLP DOI BibTeX RDF
14	Isabelle Schmidt, Nathalie Schauffel, Thomas Ellwart	Uncovering latent profiles of ICT self-concept among adults in Germany and their relation with gender.	Behav. Inf. Technol.	2024	DBLP DOI BibTeX RDF
14	Michael Houghtaling, Sandro Rama Fiorini, Nicola Fabiano, Paulo J. S. Gonçalves, Ozlem Ulgen, Tamás Haidegger, Joel Luís Carbonera, Joanna Isabelle Olszewska, Brian Page, Zvikomborero Murahwi, Edson Prestes	Standardizing an Ontology for Ethically Aligned Robotic and Autonomous Systems.	IEEE Trans. Syst. Man Cybern. Syst.	2024	DBLP DOI BibTeX RDF
14	Julian Erskine, Sébastien Briot, Isabelle Fantoni, Abdelhamid Chriette	Singularity Analysis of Rigid Directed Bearing Graphs for Quadrotor Formations.	IEEE Trans. Robotics	2024	DBLP DOI BibTeX RDF
14	Clémence Turbé, Fatima Karbou, Antoine Rabatel, Isabelle Gouttevin	Snowmelt Dynamics in a Temperate Glacier Using Sentinel-1 SAR Images: A Case Study on Saint-Sorlin Glacier, French Alps.	IEEE J. Sel. Top. Appl. Earth Obs. Remote. Sens.	2024	DBLP DOI BibTeX RDF
14	Ellen Banzhaf, Isabelle Bause, Carolin Helbig, Sebastian Elze	Personal Exposure to Environmental Pressures in Different Urban Residential Structures Linking Fieldwork and RS Mapping.	IEEE J. Sel. Top. Appl. Earth Obs. Remote. Sens.	2024	DBLP DOI BibTeX RDF
14	Frédéric Collin, Arthur Dupuy, Isabelle Parrot, Ismaël Barbara, Gérard Dray, Sophie Martin, Lionel Brunel	The effects of ambient scent on olfactory comfort and attitude toward its use in a tramway: an on-board study.	Public Transp.	2024	DBLP DOI BibTeX RDF
14	Nathaniel Li, Alexander Pan, Anjali Gopal, Summer Yue, Daniel Berrios, Alice Gatti, Justin D. Li, Ann-Kathrin Dombrowski, Shashwat Goel, Long Phan, Gabriel Mukobi, Nathan Helm-Burger, Rassin Lababidi, Lennart Justen, Andrew B. Liu, Michael Chen, Isabelle Barrass, Oliver Zhang, Xiaoyuan Zhu, Rishub Tamirisa, Bhrugu Bharathi, Adam Khoja, Zhenqi Zhao, Ariel Herbert-Voss, Cort B. Breuer, Andy Zou, Mantas Mazeika, Zifan Wang, Palash Oswal, Weiran Liu, Adam A. Hunt, Justin Tienken-Harder, Kevin Y. Shih, Kemper Talley, John Guan, Russell Kaplan, Ian Steneker, David Campbell, Brad Jokubaitis, Alex Levinson, Jean Wang, William Qian 0004, Kallol Krishna Karmakar, Steven Basart, Stephen Fitz, Mindy Levine, Ponnurangam Kumaraguru, Uday Kiran Tupakula, Vijay Varadharajan, Yan Shoshitaishvili, Jimmy Ba, Kevin M. Esvelt, Alexandr Wang, Dan Hendrycks	The WMDP Benchmark: Measuring and Reducing Malicious Use With Unlearning.	CoRR	2024	DBLP DOI BibTeX RDF
14	Xin Sun 0016, Isabelle Teljeur, Zhuying Li, Jos A. Bosch	Can a Funny Chatbot Make a Difference? Infusing Humor into Conversational Agent for Behavioral Intervention.	CoRR	2024	DBLP DOI BibTeX RDF
14	Juniper L. Lovato, Julia Witte Zimmerman, Isabelle Smith, Peter Dodds, Jennifer Karson	Foregrounding Artist Opinions: A Survey Study on Transparency, Ownership, and Fairness in AI Generative Art.	CoRR	2024	DBLP DOI BibTeX RDF