Search results for "soundness"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
7	Walid Taha, Patricia Johann	Staged Notational Definitions.	GPCE	2003	DBLP DOI BibTeX RDF
7	Bastiaan Heeren, Jurriaan Hage, S. Doaitse Swierstra	Scripting the type inference process.	ICFP	2003	DBLP DOI BibTeX RDF	domain-specific programming, constraints, type inference, directives, type errors
7	Carsten Schürmann, Jatin Shah	Representing reductions of NP-complete problems in logical frameworks: a case study.	MERLIN	2003	DBLP DOI BibTeX RDF	linear logic, NP-complete problems, logical frameworks
7	Charles Hymans	Design and Implementation of an Abstract Interpreter for VHDL.	CHARME	2003	DBLP DOI BibTeX RDF
7	Husam Abu-Haimed, Sergey Berezin, David L. Dill	Semi-formal Verification of Memory Systems by Symbolic Simulation.	CHARME	2003	DBLP DOI BibTeX RDF
7	Shaojie Wang, Sharad Malik	Synthesizing operating system based device drivers in embedded systems.	CODES+ISSS	2003	DBLP DOI BibTeX RDF	embedded system software, operating system based software synthesis, device driver, correct-by-construction
7	Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth	How to Prove Inductive Theorems? QUODLIBET!	CADE	2003	DBLP DOI BibTeX RDF
7	Renate A. Schmidt, Ullrich Hustadt	A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae.	CADE	2003	DBLP DOI BibTeX RDF
7	Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival	A static analyzer for large safety-critical software.	PLDI	2003	DBLP DOI BibTeX RDF	verification, real-time, static analysis, embedded, abstract interpretation, floating point, safety-critical software, reactive, abstract domains
7	Satoshi Yamane	Probabilistic Timed Simulation Verification and Its Application to Stepwise Refinement of Real-Time Systems.	ASIAN	2003	DBLP DOI BibTeX RDF
7	Daniele Gorla, Rosario Pugliese	Enforcing Security Policies via Types.	SPC	2003	DBLP DOI BibTeX RDF
7	François Rioult, Bruno Crémilleux	Condensed Representations in Presence of Missing Values.	IDA	2003	DBLP DOI BibTeX RDF
7	Valentin Goranko, Angelo Montanari, Guido Sciavicco	A General Tableau Method for Propositional Interval Temporal Logics.	TABLEAUX	2003	DBLP DOI BibTeX RDF
7	Christian G. Fermüller	Parallel Dialogue Games and Hypersequents for Intermediate Logics.	TABLEAUX	2003	DBLP DOI BibTeX RDF
7	Peter Thiemann 0001	Continuation-Based Partial Evaluation without Continuations.	SAS	2003	DBLP DOI BibTeX RDF	Functional programming, type systems, partial evaluation
7	Song Han 0004, Winson K. Y. Yeung, Jie Wang 0038	Identity-based confirmer signatures from pairings over elliptic curves.	EC	2003	DBLP DOI BibTeX RDF	elliptic curve discrete logarithms, identity-based signatures, Weil pairing, computational Diffie-Hellman problem
7	Takehisa Takahashi, Yuichi Umeda, Hajime Sawamura	Formal Argumentation Frameworks for the Extended Generalized Annotated Logic Programs.	KES	2003	DBLP DOI BibTeX RDF
7	Daniele Micciancio, Erez Petrank	Simulatable Commitments and Efficient Concurrent Zero-Knowledge.	EUROCRYPT	2003	DBLP DOI BibTeX RDF
7	Juan A. Garay, Philip D. MacKenzie, Ke Yang 0005	Strengthening Zero-Knowledge Protocols Using Signatures.	EUROCRYPT	2003	DBLP DOI BibTeX RDF
7	Rolf Nossum	A Contextual Approach to the Logic of Fiction.	CONTEXT	2003	DBLP DOI BibTeX RDF
7	Torben Amtoft, Robert Muller	Inferring annotated types for inter-procedural register allocation with constructor flattening.	TLDI	2003	DBLP DOI BibTeX RDF	type systems, register allocation, effects, defunctionalization, certifying compilers
7	Peeter Laud, Ricardo Corin	Sound Computational Interpretation of Formal Encryption with Composed Keys.	ICISC	2003	DBLP DOI BibTeX RDF
7	Sergio Greco, Ester Zumpano	On the rewriting and efficient computation of bound disjunctive datalog queries.	PPDP	2003	DBLP DOI BibTeX RDF	magic-set technique, logic programming, constraints, theory, disjunctive datalog
7	Dinghao Wu, Andrew W. Appel, Aaron Stump	Foundational proof checkers with small witnesses.	PPDP	2003	DBLP DOI BibTeX RDF	proof checker, proof-carrying code
7	Walter Dosch, Sönke Magnussen	Computer-Aided Refinement of Data Structures on Higher-Order Algebraic Specifications.	SERA	2003	DBLP DOI BibTeX RDF	Higher-order algebraic specification, refinement of data structure, algebraic implementation, transformation system
7	Younes Benslimane, Michel Plaisent, Prosper Bernard	Applying the Task-Technology Fit Model to WWW-based Procurement: Conceptualization and Measurement.	HICSS	2003	DBLP DOI BibTeX RDF
7	Julio Pérez, Matteo Sonza Reorda, Massimo Violante	Dependability Analysis of CAN Networks: An Emulation-Based Approach.	DFT	2003	DBLP DOI BibTeX RDF
7	Arun N. Netravali, Krishan K. Sabnani, Ramesh Viswanathan	Correct Passive Testing Algorithms and Complete Fault Coverage.	FORTE	2003	DBLP DOI BibTeX RDF
7	Ilya Shlyakhter, Robert Seater, Daniel Jackson 0001, Manu Sridharan, Mana Taghdiri	Debugging Overconstrained Declarative Models Using Unsatisfiable Cores.	ASE	2003	DBLP DOI BibTeX RDF
7	Nicoletta Fornara, Marco Colombetti	Protocol Specification Using a Commitment Based ACL.	Workshop on Agent Communication Languages	2003	DBLP DOI BibTeX RDF
7	Kess F. M. Vermeulen	More Computation Power for a Denotational Semantics for First Order Logic.	CSL	2003	DBLP DOI BibTeX RDF
7	Bernhard Reus	Modular Semantics and Logics of Classes.	CSL	2003	DBLP DOI BibTeX RDF
7	Helko Lehmann, Michael Leuschel	Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce.	LOPSTR	2003	DBLP DOI BibTeX RDF
7	Nicoletta Fornara, Marco Colombetti	Defining interaction protocols using a commitment-based agent communication language.	AAMAS	2003	DBLP DOI BibTeX RDF	open interaction system, auction, commitment, interaction protocol, agent communication language, communicative act
7	Samir Chopra, Johannes Heidema, Thomas Andreas Meyer	Some Logics of Belief and Disbelief.	Australian Conference on Artificial Intelligence	2003	DBLP DOI BibTeX RDF
7	Takamasa Koshizen, Yugo Ueda, Hiroshi Tsujino	The Brain-Like Sensorimotor Control System.	J. Intell. Robotic Syst.	2002	DBLP DOI BibTeX RDF	brain-like sensorimotor control system, unconsciousness and consciousness, prefrontal cortex, human control mechanism, minimum variance theory, humanoid robot, selective attention
7	Yunja Choi, Sanjai Rayadurgam, Mats Per Erik Heimdahl	Toward Automation for Model-Checking Requirements Specifications with Numeric Constraints.	Requir. Eng.	2002	DBLP DOI BibTeX RDF	Model checking specifications, Abstraction, Numeric constraints
7	Chengzheng Sun	Undo as concurrent inverse in group editors.	ACM Trans. Comput. Hum. Interact.	2002	DBLP DOI BibTeX RDF	distributed systems, computer-supported cooperative work, concurrency control, REDUCE, operational transformation, collaborative applications, consistence maintenance, Group undo
7	Cherng-Min Ma, Shu-Yen Wan, Jiann-Der Lee	Three-Dimensional Topology Preserving Reduction on the 4-Subfields.	IEEE Trans. Pattern Anal. Mach. Intell.	2002	DBLP DOI BibTeX RDF	connectivity preservation, 3D thinning algorithm, 4-subfield thinning, thinning, Topology preservation
7	Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran	An assume-guarantee rule for checking simulation.	ACM Trans. Program. Lang. Syst.	2002	DBLP DOI BibTeX RDF	verification rules, Simulation relations
7	Maurizio Pighin, Vili Podgorelec, Peter Kokol	Program Risk Definition via Linear Programming Techniques.	IEEE METRICS	2002	DBLP DOI BibTeX RDF
7	Richard Jüllig	Formal Methods in Enterprise Computing.	ICFEM	2002	DBLP DOI BibTeX RDF
7	Jonathan Aldrich, Valentin Kostadinov, Craig Chambers	Alias annotations for program understanding.	OOPSLA	2002	DBLP DOI BibTeX RDF	aliasjava, java, type inference, aliasing, encapsulation, ownership types, uniqueness
7	Carmen Graciani Díaz, Francisco-Jesús Martín-Mateos, Mario J. Pérez-Jiménez	Specification of Adleman's Restricted Model Using an Automated Reasoning System: Verification of Lipton's Experiment.	UMC	2002	DBLP DOI BibTeX RDF
7	Sara Comai, Letizia Tanca	Editorial message: special track on web and E-business applications.	SAC	2002	DBLP DOI BibTeX RDF
7	Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni	A Syntactic Approach to Foundational Proof-Carrying Code.	LICS	2002	DBLP DOI BibTeX RDF
7	Sophie Laplante, Richard Lassaigne, Frédéric Magniez, Sylvain Peyronnet, Michel de Rougemont	Probabilistic Abstraction for Model Checking: An Approach Based on Property Testing.	LICS	2002	DBLP DOI BibTeX RDF
7	Bernhard Reus, Thomas Streicher	Semantics and Logic of Object Calculi.	LICS	2002	DBLP DOI BibTeX RDF
7	Niels Jørgensen	Safeness of Make-Based Incremental Recompilation.	FME	2002	DBLP DOI BibTeX RDF	incremental recompilation, semantic model, Make
7	François Pottier, Vincent Simonet	Information flow inference for ML.	POPL	2002	DBLP DOI BibTeX RDF
7	George C. Necula, Scott McPeak, Westley Weimer	CCured: type-safe retrofitting of legacy code.	POPL	2002	DBLP DOI BibTeX RDF
7	Jonas Holmerin	Improved Inapproximability Results for Vertex Cover on k -Uniform Hypergraphs.	ICALP	2002	DBLP DOI BibTeX RDF
7	Paolo Mancarella, Dino Pedreschi, Salvatore Ruggieri	Negation as Failure through Abduction: Reasoning about Termination.	Computational Logic: Logic Programming and Beyond	2002	DBLP DOI BibTeX RDF
7	Jörg H. Siekmann, Graham Wrightson	An Open Research Problem: Strong Completeness of R. Kowalski's Connection Graph Proof Procedure.	Computational Logic: Logic Programming and Beyond	2002	DBLP DOI BibTeX RDF
7	Michel Benaroch	Specifying Local Ontologies in Support of Semantic Interoperability of Distributed Inter-organizational Applications.	NGITS	2002	DBLP DOI BibTeX RDF
7	Nobuko Yoshida, Kohei Honda 0001, Martin Berger 0001	Linearity and Bisimulation.	FoSSaCS	2002	DBLP DOI BibTeX RDF
7	Hongseok Yang, Peter W. O'Hearn	A Semantic Basis for Local Reasoning.	FoSSaCS	2002	DBLP DOI BibTeX RDF
7	Brigitte Pientka	A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming.	ICLP	2002	DBLP DOI BibTeX RDF
7	Pedro Cabalar	A Rewriting Method for Well-Founded Semantics with Explicit Negation.	ICLP	2002	DBLP DOI BibTeX RDF
7	Till Mossakowski	Comorphism-Based Grothendieck Logics.	MFCS	2002	DBLP DOI BibTeX RDF
7	Alexandre Miquel, Benjamin Werner	The Not So Simple Proof-Irrelevant Model of CC.	TYPES	2002	DBLP DOI BibTeX RDF
7	Wil M. P. van der Aalst, Alexander Hirnschall, H. M. W. Verbeek	An Alternative Way to Analyze Workflow Graphs.	CAiSE	2002	DBLP DOI BibTeX RDF
7	Robert Bruce Findler, Matthias Felleisen	Contracts for higher-order functions.	ICFP	2002	DBLP DOI BibTeX RDF	predicate typing, solfware reliability, contracts, behavioral specifications, higher-order functions
7	Matthias Neubauer, Peter Thiemann 0001	Type classes with more higher-order polymorphism.	ICFP	2002	DBLP DOI BibTeX RDF	higher-order unification, Haskell, type inference, type classes
7	Ivan Damgård, Eiichiro Fujisaki	A Statistically-Hiding Integer Commitment Scheme Based on Groups with Hidden Order.	ASIACRYPT	2002	DBLP DOI BibTeX RDF
7	Jonathan Ford, Natarajan Shankar	Formal Verification of a Combination Decision Procedure.	CADE	2002	DBLP DOI BibTeX RDF
7	Mauro Ferrari 0002, Camillo Fiorentini, Guido Fiorino	Tableau Calculi for the Logics of Finite k-Ary Trees.	TABLEAUX	2002	DBLP DOI BibTeX RDF
7	Alfredo De Santis, Giovanni Di Crescenzo, Giuseppe Persiano	Randomness-Optimal Characterization of Two NP Proof Systems.	RANDOM	2002	DBLP DOI BibTeX RDF
7	Jeff Z. Pan, Ian Horrocks 0001	Extending Datatype Support in Web Ontology Reasoning.	OTM	2002	DBLP DOI BibTeX RDF
7	Xiaohui Gu, Klara Nahrstedt	Dynamic QoS-Aware Multimedia Service Configuration in Ubiquitous Computing Environments.	ICDCS	2002	DBLP DOI BibTeX RDF
7	Alea M. Fairchild	Knowledge Management Metrics via a Balanced Scorecard Methodology.	HICSS	2002	DBLP DOI BibTeX RDF	Knowledge Utilization, IS Investment, Management Issues
7	Anna Ciampolini, Evelina Lamma, Paola Mello, Paolo Torroni	A Proof-System for the Safe Execution of Tasks in Multi-agent Systems.	JELIA	2002	DBLP DOI BibTeX RDF
7	Sava Krstic, John Matthews	Verifying BDD Algorithms through Monadic Interpretation.	VMCAI	2002	DBLP DOI BibTeX RDF
7	Didier Galmiche, Daniel Méry, David J. Pym	Resource Tableaux.	CSL	2002	DBLP DOI BibTeX RDF
7	Dipankar Sarkar 0001	Register Transfer Operation Analysis during Data Path Verification.	ASP-DAC/VLSI Design	2002	DBLP DOI BibTeX RDF	Sequential Circuit Verification, Control Part - Data Path, Data Path Verification, RTL Behaviours
7	Seyoon Tak, Oh-Young Song, Hyeong-Seok Ko	Spacetime Sweeping: An Interactive Dynamic Constraints Solver.	CA	2002	DBLP DOI BibTeX RDF
7	Boaz Barak, Oded Goldreich 0001	Universal Arguments and their Applications.	CCC	2002	DBLP DOI BibTeX RDF	Probabilistic proof systems, computationally-sound proof systems, zero-knowledge proof systems, probabilistic checkable proofs (PCP), collision-free hashing, witness indistinguishable proof systems, error-correcting codes, proofs of knowledge
7	Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina	Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers.	LOPSTR	2002	DBLP DOI BibTeX RDF
7	Rolf Nossum, Luciano Serafini	Multicontext Logic for Semigroups of Contexts.	AISC	2002	DBLP DOI BibTeX RDF	Integration of Logical Reasoning and Computer Algebra, Logic and Symbolic Computing, Reasoning
7	Deepak Kapur	A Rewrite Rule Based Framework for Combining Decision Procedures.	FroCoS	2002	DBLP DOI BibTeX RDF
7	Joaquim Armengol, Josep Vehí, Louise Travé-Massuyès, Miguel Ángel Sainz	Application of Modal Intervals to the Generation of Error-Bounded Envelopes.	Reliab. Comput.	2001	DBLP DOI BibTeX RDF
7	Ch. Nikolarakos, N. Georgopoulos	Sourcing: Issues to be considered for the make-or-buy decisions.	Oper. Res.	2001	DBLP DOI BibTeX RDF	Strategy, Competitive advantage, Sourcing, Vertical integration
7	Carlos Caleiro, Paulo Mateus, Jaime Ramos, Amílcar Sernadas	Combining Logics: Parchments Revisited.	WADT	2001	DBLP DOI BibTeX RDF
7	Carsten Schürmann	A Type-Theoretic Approach to Induction with Higher-Order Encodings.	LPAR	2001	DBLP DOI BibTeX RDF
7	Hans Hagen, Achim Ebert, Rolf Hendrik van Lengen, Gerik Scheuermann	Scientific Visualization - Methods and Applications.	Informatics	2001	DBLP DOI BibTeX RDF
7	Oscar Fontenla-Romero, Bertha Guijarro-Berdiñas, Amparo Alonso-Betanzos	A Functional-Neural Network for Post-Nonlinear Independent Component Analysis.	IWANN (1)	2001	DBLP DOI BibTeX RDF
7	Michael T. Hallett, Jens Lagergren	Efficient algorithms for lateral gene transfer problems.	RECOMB	2001	DBLP DOI BibTeX RDF
7	Steffen Helke, Florian Kammüller	Representing Hierarchical Automata in Interactive Theorem Provers.	TPHOLs	2001	DBLP DOI BibTeX RDF
7	Pavel Naumov, Mark-Oliver Stehr, José Meseguer 0001	The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability).	TPHOLs	2001	DBLP DOI BibTeX RDF
7	Mark-Oliver Stehr, José Meseguer 0001, Peter Csaba Ölveczky	Rewriting Logic as a Unifying Framework for Petri Nets.	Unifying Petri Nets	2001	DBLP DOI BibTeX RDF
7	Kouta Kanda, Makoto Haraguchi, Yoshiaki Okubo	Constructing Approximate Informative Basis of Association Rules.	Discovery Science	2001	DBLP DOI BibTeX RDF
7	Geoffrey Smith 0001	A New Type System for Secure Information Flow.	CSFW	2001	DBLP DOI BibTeX RDF
7	Peter Sewell	Modules, abstract types, and distributed versioning.	POPL	2001	DBLP DOI BibTeX RDF
7	Darius Blasband	Parsing in a Hostile World.	WCRE	2001	DBLP DOI BibTeX RDF
7	Michael Huth 0001, Radha Jagadeesan, David A. Schmidt	Modal Transition Systems: A Foundation for Three-Valued Program Analysis.	ESOP	2001	DBLP DOI BibTeX RDF
7	Sylvain Conchon, François Pottier	JOIN(X): Constraint-Based Type Inference for the Join-Calculus.	ESOP	2001	DBLP DOI BibTeX RDF
7	Takamasa Koshizen, Hiroshi Tsujino	Hypothetically Modeled Perceptual Sensory Modality of Human Vision Selective Attention Scheme by PFC-Based Network.	RobVis	2001	DBLP DOI BibTeX RDF
7	Sophia Drossopoulou, Ferruccio Damiani, Mariangiola Dezani-Ciancaglini, Paola Giannini	Fickle : Dynamic Object Re-classification.	ECOOP	2001	DBLP DOI BibTeX RDF
7	David G. Clarke, James Noble 0001, John Potter	Simple Ownership Types for Object Containment.	ECOOP	2001	DBLP DOI BibTeX RDF	OO type systems, object containment, flexible alias protection, ownership types
7	Wil M. P. van der Aalst, H. M. W. Verbeek, Akhil Kumar 0001	Verification of XRL: An XML-based Workflow Language.	CSCWD	2001	DBLP DOI BibTeX RDF