|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 1960 occurrences of 846 keywords
|
|
|
Results
Found 3383 publication records. Showing 3383 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
21 | Hongbo Li 0012, Lei Huang |
Complex brackets, balanced complex differences, and applications in symbolic geometric computing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISSAC ![In: Symbolic and Algebraic Computation, International Symposium, ISSAC 2008, Linz/Hagenberg, Austria, July 20-23, 2008, Proceedings, pp. 181-188, 2008, ACM, 978-1-59593-904-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
bracket algebra, complex numbers method, graph theory, theorem proving, geometric algebra |
21 | Viorica Sofronie-Stokkermans |
On unification for bounded distributive lattices. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 8(2), pp. 12, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
decision procedures for the positive theory, Theorem proving, unification, distributive lattices, SAT solving |
21 | Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump |
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 31(3), pp. 221-239, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Competition, Decision procedures, Automated theorem proving, SMT, Satisfiability modulo theories |
21 | Greg Bronevetsky, Bronis R. de Supinski |
Complete Formal Specification of the OpenMP Memory Model. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Parallel Program. ![In: Int. J. Parallel Program. 35(4), pp. 335-392, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
parallel programming, theorem proving, OpenMP, formal systems |
21 | Swen Jacobs, Uwe Waldmann |
Comparing Instance Generation Methods for Automated Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 38(1-3), pp. 57-78, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
disconnection calculus, primal partial instantiation, resolution-based instance generation, theorem proving, automated reasoning |
21 | Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli |
User Interaction with the Matita Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 39(2), pp. 109-139, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Mathematical knowledge management, XML, Digital libraries, Authoring, Interactive theorem proving, Proof assistant |
21 | Julien Narboux |
A Graphical User Interface for Formal Proofs in Geometry. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 39(2), pp. 161-180, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Interface, Geometry, Automated theorem proving, Theorem prover, Proof assistant, Coq, Dynamic geometry |
21 | Alberto Ciaffaglione, Luigi Liquori, Marino Miculan |
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 39(1), pp. 1-47, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Functional and imperative object-calculi, Logical foundations of programming, Coinductive type theories, Logical frameworks, Interactive theorem proving |
21 | Reinhold Letz, Gernot Stenz |
The Disconnection Tableau Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 38(1-3), pp. 79-126, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
disconnection tableaux, theorem proving |
21 | Wenjun Wu 0003, Xiao-Shan Gao |
Mathematics mechanization and applications after thirty years. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Frontiers Comput. Sci. China ![In: Frontiers Comput. Sci. China 1(1), pp. 1-8, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
mathematics mechanization, characteristic set method, automated theorem discovering, symbolic equation solving, intelligent computer-aided design, computer vision, robotics, automated theorem proving, computer aided geometric design |
21 | Damián Barsotti, Leonor Prensa Nieto, Alwen Tiu |
Verification of clock synchronization algorithms: experiments on a combination of deductive tools. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 19(3), pp. 321-341, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Combination of deductive tools, Verification, Theorem proving, Clock synchronization |
21 | Paul Curzon, Rimvydas Ruksenas, Ann Blandford |
An approach to formal verification of human-computer interaction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 19(4), pp. 513-550, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Formal cognitive architecture, Formal verification, Theorem proving, Interactive systems, Human error |
21 | Chris Lesniewski-Laas, Bryan Ford, Jacob Strauss, Robert Tappan Morris, M. Frans Kaashoek |
Alpaca: extensible authorization for distributed services. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CCS ![In: Proceedings of the 2007 ACM Conference on Computer and Communications Security, CCS 2007, Alexandria, Virginia, USA, October 28-31, 2007, pp. 432-444, 2007, ACM, 978-1-59593-703-2. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
security, cryptography, authorization, theorem-proving, logic |
21 | Shoichi Morimoto, Shinjiro Shigematsu, Yuichi Goto, Jingde Cheng |
Formal verification of security specifications with common criteria. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 2007 ACM Symposium on Applied Computing (SAC), Seoul, Korea, March 11-15, 2007, pp. 1506-1512, 2007, ACM, 1-59593-480-4. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
ISO/IEC 15408, theorem-proving, Z notation |
21 | Yongjian Li |
Mechanized proofs for the parameter abstraction and guard strengthening principle in parameterized verification of cache coherence protocols. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 2007 ACM Symposium on Applied Computing (SAC), Seoul, Korea, March 11-15, 2007, pp. 1534-1535, 2007, ACM, 1-59593-480-4. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
parameterized verification, theorem proving, symmetry |
21 | Harvey Tuch, Gerwin Klein, Michael Norrish |
Types, bytes, and separation logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pp. 97-108, 2007, ACM, 1-59593-575-4. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
C, separation logic, interactive theorem proving |
21 | Leo Freitas, Jim Woodcock 0001 |
Proving Theorems About JML Classes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods and Hybrid Real-Time Systems ![In: Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bjørner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, pp. 255-279, 2007, Springer, 978-3-540-75220-2. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Grand Challenge in Verified Software, Java Collections Framework, Java HashMap class, linking theories, Z/Eves, formal specification, Z, software verification, JML, Java Modeling Language, mechanical theorem proving, Verified Software Repository |
21 | Leonard Lensink, Sjaak Smetsers, Marko C. J. D. van Eekelen |
Machine Checked Formal Proof of a Scheduling Protocol for Smartcard Personalization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMICS ![In: Formal Methods for Industrial Critical Systems, 12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers, pp. 115-132, 2007, Springer, 978-3-540-79706-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
simulation, verification, theorem proving, PVS, cyclic scheduling |
21 | Christian Engel 0002, Reiner Hähnle |
Generating Unit Tests from Formal Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TAP ![In: Tests and Proofs - 1st International Conference, TAP 2007, Zurich, Switzerland, February 12-13, 2007. Revised Papers, pp. 169-188, 2007, Springer, 978-3-540-73769-8. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
theorem proving, program verification, model-based testing, unit testing, symbolic execution, test coverage, white-box testing |
21 | Achim D. Brucker, Burkhart Wolff |
Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TAP ![In: Tests and Proofs - 1st International Conference, TAP 2007, Zurich, Switzerland, February 12-13, 2007. Revised Papers, pp. 149-168, 2007, Springer, 978-3-540-73769-8. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
symbolic test case generations, theorem proving, computer security, black box testing, Isabelle/HOL, test sequence generation |
21 | Felicidad Aguado, José Luis Doncel, José María Molinelli, Gilberto Pérez 0001, Concepción Vidal, Ana María Vieites |
Certified Genetic Algorithms: Crossover Operators for Permutations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROCAST ![In: Computer Aided Systems Theory - EUROCAST 2007, 11th International Conference on Computer Aided Systems Theory, Las Palmas de Gran Canaria, Spain, February 12-16, 2007, Revised Selected Papers, pp. 282-289, 2007, Springer, 978-3-540-75866-2. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Calculus of Inductive Constructions, Genetic Algorithm, Specification, Theorem Proving, Crossover, Coq |
21 | Guillaume Burel, Claude Kirchner |
Cut Elimination in Deduction Modulo by Abstract Completion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFCS ![In: Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, NY, USA, June 4-7, 2007, Proceedings, pp. 115-131, 2007, Springer, 978-3-540-72732-3. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Knuth-Bendix completion, automated deduction and interactive theorem proving, proof ordering, abstract canonical system, cut elimination, deduction modulo |
21 | Hongbo Li 0012 |
A recipe for symbolic geometric computing: long geometric product, BREEFS and Clifford factorization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISSAC ![In: Symbolic and Algebraic Computation, International Symposium, ISSAC 2007, Waterloo, Ontario, Canada, July 28 - August 1, 2007, Proceedings, pp. 261-268, 2007, ACM, 978-1-59593-743-8. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
null bracket algebra, symbolic geometric computing, geometric invariance, geometric theorem proving, conformal geometric algebra |
21 | Anatoli Degtyarev, Michael Fisher 0001, Boris Konev |
Monodic temporal resolution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 7(1), pp. 108-150, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Temporal logic, resolution, automated theorem proving |
21 | Lawrence C. Paulson |
Defining functions on equivalence classes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 7(4), pp. 658-675, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
theorem proving, Equivalence classes, quotients |
21 | Jozef Hooman, Mark van der Zwaag |
A semantics of communicating reactive objects with timing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 8(2), pp. 97-112, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
UML, Real-time, Formal methods, Theorem proving, Formal semantics |
21 | Chung-Hsien Wu, Jui-Feng Yeh, Yu-Sheng Lai |
Semantic Segment Extraction and Matching for Internet FAQ Retrieval. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Knowl. Data Eng. ![In: IEEE Trans. Knowl. Data Eng. 18(7), pp. 930-940, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
deduction and theorem proving, Natural language processing, query formulation, retrieval models, knowledge processing |
21 | Nick C. Fiala, Keith M. Agre |
Searching for Shortest Single Axioms for Groups of Exponent 6. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 36(3), pp. 241-257, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
exponent, single axiom, group, automated theorem-proving |
21 | Oliver Pell |
Verification of FPGA Layout Generators in Higher-Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 37(1-2), pp. 117-152, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
layout description, circuit verification, FPGA, theorem proving |
21 | Ruqian Lu, Daniel Dajun Zeng, Fei-Yue Wang 0001 |
AI Research in China: 50 Years down the Road. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Intell. Syst. ![In: IEEE Intell. Syst. 21(3), pp. 91-93, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
AI in China, intelligence science, computer art and animation, knowware, geometrical theorem proving |
21 | Gerwin Klein, Tobias Nipkow |
A machine-checked model for a Java-like language, virtual machine, and compiler. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Program. Lang. Syst. ![In: ACM Trans. Program. Lang. Syst. 28(4), pp. 619-695, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Java, theorem proving, operational semantics |
21 | Antonio Montes, Tomás Recio |
Automatic Discovery of Geometry Theorems Using Minimal Canonical Comprehensive Gröbner Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry, 6th International Workshop, ADG 2006, Pontevedra, Spain, August 31-September 2, 2006. Revised Papers, pp. 113-138, 2006, Springer, 978-3-540-77355-9. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
automatic discovering, comprehensive Gröbner system, canonical Gröbner system, automatic theorem proving |
21 | Erik Reeber, Jun Sawada |
Combining ACL2 and an automated verification tool to verify a multiplier. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 63-70, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
model checking, theorem proving, hardware verification |
21 | Warren A. Hunt Jr., Erik Reeber |
A SAT-based procedure for verifying finite state machines in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 127-135, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
satisfiability solving, theorem proving, hardware verification, ACL2 |
21 | Julien Schmaltz, Dominique Borrione |
Towards a formal theory of on chip communications in the ACL2 logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 47-56, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
formal theory, network on a chip, theorem proving, communication theory |
21 | David S. Hardin, Eric W. Smith, William D. Young |
A robust machine code proof framework for highly secure applications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 11-20, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
cryptography, theorem proving, certification, symbolic simulation, ACL2, high-assurance, processor modeling |
21 | Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard, John D. McLean |
Formal specification and verification of data separation in a separation kernel for an embedded system. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CCS ![In: Proceedings of the 13th ACM Conference on Computer and Communications Security, CCS 2006, Alexandria, VA, USA, October 30 - November 3, 2006, pp. 346-355, 2006, ACM. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
code verification, formal specification, theorem proving, formal model, separation kernel |
21 | Shoichi Morimoto, Shinjiro Shigematsu, Yuichi Goto, Jingde Cheng |
A security specification verification technique based on the international standard ISO/IEC 15408. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 2006 ACM Symposium on Applied Computing (SAC), Dijon, France, April 23-27, 2006, pp. 1802-1803, 2006, ACM, 1-59593-108-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
theorem-proving, Z notation, common criteria |
21 | Shuvendu K. Lahiri, Shaz Qadeer |
Verifying properties of well-founded linked lists. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, pp. 115-126, 2006, ACM, 1-59593-027-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
first-order axiomatization, heap abstraction, well-founded linked lists, decision procedure, automated theorem proving |
21 | Ewen Denney, Bernd Fischer 0002 |
A generic annotation inference algorithm for the safety certification of automatically generated code. ![Search on Bibsonomy](Pics/bibsonomy.png) |
GPCE ![In: Generative Programming and Component Engineering, 5th International Conference, GPCE 2006, Portland, Oregon, USA, October 22-26, 2006, Proceedings, pp. 121-130, 2006, ACM, 1-59593-237-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
hoare calculus, logical annotations, program verification, automated theorem proving, software certification, automated code generation |
21 | Christian Jacobi 0002, Christoph Berg |
Formal Verification of the VAMP Floating Point Unit. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 26(3), pp. 227-266, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
IEEE standard 754, formal verification, theorem proving, PVS, floating point unit |
21 | Milos Besta, Frank A. Stomp |
A Complete Mechanization of Correctness of a String-Preprocessing Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 27(1-2), pp. 5-17, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
formal methods, pattern matching, theorem proving, PVS |
21 | Behzad Akbarpour, Sofiène Tahar, Abdelkader Dekdouk |
Formalization of Fixed-Point Arithmetic in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 27(1-2), pp. 173-200, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
theorem-proving, floating-point arithmetic, fixed-point arithmetic, HOL |
21 | Jewgenij Botaschanjan, Leonid Kof, C. Kühnel, Maria Spichkova |
Towards verified automotive software. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM SIGSOFT Softw. Eng. Notes ![In: ACM SIGSOFT Softw. Eng. Notes 30(4), pp. 1-6, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
verification, integration, theorem proving, automotive, time-triggered, model based software engineering |
21 | David Detlefs, Greg Nelson, James B. Saxe |
Simplify: a theorem prover for program checking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 52(3), pp. 365-473, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
Theorem proving, decision procedures, program checking |
21 | Bernard Jurkowiak, Chu Min Li, Gil Utard |
A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 34(1), pp. 73-101, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
parallelism, automated theorem proving, SAT problem |
21 | M. Carmen Fernández Gago, Ullrich Hustadt, Clare Dixon, Michael Fisher 0001, Boris Konev |
First-Order Temporal Verification in Practice. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 34(3), pp. 295-321, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
temporal logics of knowledge, theorem proving, resolution, first-order temporal logic |
21 | Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa |
Tool-Assisted Specification and Verification of Typed Low-Level Languages. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 35(4), pp. 295-354, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
virtual machine, theorem proving, Java Card, bytecode verification |
21 | Rohit Gheyi, Tiago Massoni |
Formal refactorings for object models. ![Search on Bibsonomy](Pics/bibsonomy.png) |
OOPSLA Companion ![In: Companion to the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2005, October 16-20, 2005, San Diego, CA, USA, pp. 208-209, 2005, ACM, 1-59593-193-7. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
theorem proving, object models, model refactoring |
21 | Bart Jacobs 0001, Wolter Pieters, Martijn Warnier |
Statically checking confidentiality via dynamic labels. ![Search on Bibsonomy](Pics/bibsonomy.png) |
WITS ![In: Proceedings of the POPL 2005 Workshop on Issues in the Theory of Security, WITS 2005, Long Beach, California, USA, January 10-11, 2005, pp. 50-56, 2005, ACM, 1-58113-980-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
(Higher Order) theorem proving, formal verification, static analysis, abstract interpretation, confidentiality |
21 | Olha Shkaravska |
Types with semantics: soundness proof assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005, pp. 50-57, 2005, ACM, 978-1-59593-072-9. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
type system, assertion, automated theorem proving, program logic |
21 | Kevin Donnelly, Hongwei Xi |
Combining higher-order abstract syntax with first-order abstract syntax in ATS. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005, pp. 58-63, 2005, ACM, 978-1-59593-072-9. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
ATS/LF, theorem proving, dependent types, higher-order abstract syntax, ATS |
21 | Yuki Chiba, Takahito Aoto 0001, Yoshihito Toyama |
Program transformation by templates based on term rewriting. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 11-13 2005, Lisbon, Portugal, pp. 59-69, 2005, ACM, 1-59593-090-6. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
inductive theorem proving, tree homomorphism, program transformation, term rewriting |
21 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Equational Approach to Formal Analysis of TLS. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICDCS ![In: 25th International Conference on Distributed Computing Systems (ICDCS 2005), 6-10 June 2005, Columbus, OH, USA, pp. 795-804, 2005, IEEE Computer Society, 0-7695-2331-5. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
security, verification, algebraic specification, rewriting, interactive theorem proving |
21 | Rohit Gheyi, Tiago Massoni, Paulo Borba |
A rigorous approach for proving model refactorings. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASE ![In: 20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005), November 7-11, 2005, Long Beach, CA, USA, pp. 372-375, 2005, ACM, 1-58113-993-4. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
theorem proving, model refactoring |
21 | Jan Jürjens, Mark Yampolskiy |
Code security analysis with assertions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASE ![In: 20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005), November 7-11, 2005, Long Beach, CA, USA, pp. 392-395, 2005, ACM, 1-58113-993-4. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
code security analysis, cryto-based software, cryptographic protocols, first-order logic, assertions, automated theorem proving, C programs |
21 | Subash Shankar, Sinan Asa, Vladimir Sipos, Xiaowei Xu |
Reasoning about real-time statecharts in the presence of semantic variations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASE ![In: 20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005), November 7-11, 2005, Long Beach, CA, USA, pp. 243-252, 2005, ACM, 1-58113-993-4. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
model checking, semantics, temporal logics, theorem proving, statecharts |
21 | Gudmund Grov |
Verifying the correctness of hume programs: an approach combining deductive and algorithmic reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASE ![In: 20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005), November 7-11, 2005, Long Beach, CA, USA, pp. 444-447, 2005, ACM, 1-58113-993-4. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
model checking, formal methods, formal verification, theorem proving, specification languages |
21 | Fatma Ozcan, V. S. Subrahmanian, Jürgen Dix |
Improving Performance of Heterogeneous Agents. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Ann. Math. Artif. Intell. ![In: Ann. Math. Artif. Intell. 41(2-4), pp. 339-395, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
deduction and theorem proving, multi-agency, logical foundations, multi-agent reasoning, interoperability, distributed AI, heterogenous data sources |
21 | Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirli Kaynar, Nancy A. Lynch |
Using simulated execution in verifying distributed algorithms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 6(1), pp. 67-76, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
Invariant detection, Static analysis, Theorem proving, Dynamic analysis |
21 | Christoph Walther, Stephan Schweitzer |
Verification in the Classroom. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 32(1), pp. 35-73, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
computer uses in education, deduction and automated theorem proving, computer-aided verification |
21 | Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan 0001, I. V. Ramakrishnan |
An unfold/fold transformation framework for definite logic programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Program. Lang. Syst. ![In: ACM Trans. Program. Lang. Syst. 26(3), pp. 464-509, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
inductive theorem proving, Logic programming, program transformation, unfolding, folding |
21 | César A. Muñoz, Gilles Dowek, Victor Carreño |
Modeling and verification of an air traffic concept of operations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISSTA ![In: Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, Boston, Massachusetts, USA, July 11-14, 2004, pp. 175-182, 2004, ACM, 1-58113-820-2. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
air traffic management systems, model checking, theorem proving |
21 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Equational Approach to Formal Verification of SET. ![Search on Bibsonomy](Pics/bibsonomy.png) |
QSIC ![In: 4th International Conference on Quality Software (QSIC 2004), 8-10 September 2004, Braunschweig, Germany, pp. 50-59, 2004, IEEE Computer Society, 0-7695-2207-6. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
security, verification, algebraic specification, rewriting, interactive theorem proving, payment |
21 | Hongbo Li 0012 |
Symbolic computation in the homogeneous geometric model with clifford algebra. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISSAC ![In: Symbolic and Algebraic Computation, International Symposium ISSAC 2004, Santander, Spain, July 4-7, 2004, Proceedings, pp. 221-228, 2004, ACM, 1-58113-827-X. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
homogeneous model, automated theorem proving, symbolic computation, geometric algebra, clifford algebra |
21 | Marcelo Glusman, Shmuel Katz |
A Mechanized Proof Environment for the Convenient Computations Proof Method. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 23(2), pp. 115-142, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
convenient computations, proof environment, deductive theorem proving, formal verification, PVS |
21 | John Harrison 0001 |
Formal Verification of Square Root Algorithms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 22(2), pp. 143-153, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
formal verification, floating-point arithmetic, automated theorem proving |
21 | Susanne Graf |
Preface by the section editor. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 4(2), pp. 139-141, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
Goals: Conformance testing, Formal verification Techniques: Static analysis, Tool integration Application domains: Asynchronous systems, Performance evaluation, Model-checking, Markov chains, Theorem proving, Security protocols, Slicing, Partial-order reductions, Probabilistic systems, Component-based approaches |
21 | Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Thomas F. Melham |
The PROSPER toolkit. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 4(2), pp. 189-210, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
Proof engine, Formal verification, Theorem proving, Tool integration |
21 | Jonathan Ford, Ian A. Mason |
Formal Foundations of Operational Semantics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
High. Order Symb. Comput. ![In: High. Order Symb. Comput. 16(3), pp. 161-202, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
contexts, theorem proving, operational semantics, PVS, calculus |
21 | Gerwin Klein, Martin Wildmoser |
Verified Bytecode Subroutines. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 30(3-4), pp. 363-398, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
Java, theorem proving, subroutines, dataflow analysis, Isabelle, bytecode verification |
21 | Jei-Wen Teng, Yih-Kuen Tsay |
Composing Temporal-Logic Specifications with Machine Assistance. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003, Proceedings, pp. 719-738, 2003, Springer, 3-540-40828-2. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
Assumption-Guarantee, Compositional Specification, Formal Correctness, Temporal Logic, Theorem Proving, Concurrent Systems, PVS, Compositional Verification, Component-Based Software |
21 | Alberto Ciaffaglione, Luigi Liquori, Marino Miculan |
Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
logical foundations of programming, object-based calculi with side-effects, program and system verification, logical frameworks, interactive theorem proving |
21 | Michael Norrish |
Mechanising Hankin and Barendregt using the Gordon-Melham axioms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
higher order abstract syntax, interactive theorem-proving |
21 | Yasuhiko Minamide, Koji Okuma |
Verifying CPS transformations in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
program transformation, theorem proving, correctness proofs |
21 | Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant |
A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DAC ![In: Proceedings of the 40th Design Automation Conference, DAC 2003, Anaheim, CA, USA, June 2-6, 2003, pp. 425-430, 2003, ACM, 1-58113-688-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
theorem proving, decision procedures, boolean satisfiability, design verification |
21 | Karthikeyan Bhargavan, Davor Obradovic, Carl A. Gunter |
Formal verification of standards for distance vector routing protocols. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 49(4), pp. 538-576, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
distance vector routing, network standards, model checking, Formal verification, routing protocols, AODV, SPIN, interactive theorem proving, HOL, RIP |
21 | Peter Frey, Radharamanan Radhakrishnan, Harold W. Carter, Philip A. Wilsey, Perry Alexander |
A Formal Specification and Verification Framework for Time Warp-Based Parallel Simulation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 28(1), pp. 58-78, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
formal specification, formal verification, theorem proving, time warp, parallel discrete event simulation |
21 | Jon Whittle 0001, Alan Bundy, Richard J. Boulton |
Proofs-as-Programs as a Framework for the Design of an Analogy-Based ML Editor. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 13(3-5), pp. 403-421, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
Programming environments, Functional programming, Theorem proving |
21 | J Strother Moore, George Porter |
The apprentice challenge. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Program. Lang. Syst. ![In: ACM Trans. Program. Lang. Syst. 24(3), pp. 193-216, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
Java, theorem proving, Java Virtual Machine, mutual exclusion, operational semantics, parallel and distributed computation |
21 | Jozef Hooman, Jaco van de Pol |
Formal verification of replication on a distributed data space architecture. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 2002 ACM Symposium on Applied Computing (SAC), March 10-14, 2002, Madrid, Spain, pp. 351-358, 2002, ACM, 1-58113-445-2. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
data space architecture, model-checking, formal verification, coordination, theorem proving |
21 | J Strother Moore |
Functional formal methods. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002., pp. 123, 2002, ACM, 1-58113-487-8. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
functional programming, Java Virtual Machine, microarchitecture, software verification, Common Lisp, hardware verification, mechanical theorem proving |
21 | Steven Shapiro, Yves Lespérance, Hector J. Levesque |
The cognitive agents specification language and verification environment for multiagent systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AAMAS ![In: The First International Joint Conference on Autonomous Agents & Multiagent Systems, AAMAS 2002, July 15-19, 2002, Bologna, Italy, Proceedings, pp. 19-26, 2002, ACM. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
agent specification languages, theorem proving, proof assistants, verification tools |
21 | Michael Fisher 0001, Clare Dixon, Martin Peim |
Clausal temporal resolution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 2(1), pp. 12-56, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
temporal logic, theorem proving, resolution |
21 | Raymond Reiter |
On knowledge-based programming with sensing in the situation calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 2(4), pp. 433-457, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
dynamic closed-world assumption, sensing and knowledge, situation calculus programming languages, theorem-proving, situation calculus |
21 | Andrei Voronkov |
How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 2(2), pp. 182-215, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
theorem proving, modal logic, description logics, proof-search, inverse method |
21 | Maria Luisa Bonet, Nicola Galesi |
Optimality of size-width tradeoffs for resolution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. Complex. ![In: Comput. Complex. 10(4), pp. 261-276, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
complexity of proofs, automated theorem proving.¶ Subject classification. 03F20, 03B05, Resolution, 68T15 |
21 | Jörg H. Siekmann, Graham Wrightson |
Erratum: a counterexample to W. Bibel's and E. Eder's strong completeness result for connection graph resolution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 48(1), pp. 145-147, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
computational logic, mechanical theorem proving, mathematical logic |
21 | David A. Basin, Harald Ganzinger |
Automated complexity analysis based on ordered resolution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 48(1), pp. 70-109, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
ordered resolution, automated theorem proving, complexity analysis, first-order theories |
21 | Angelo Gargantini, Angelo Morzenti |
Automated deductive requirements analysis of critical systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Softw. Eng. Methodol. ![In: ACM Trans. Softw. Eng. Methodol. 10(3), pp. 255-307, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
finite variability, temporal logic, theorem proving, hybrid systems, state-transition systems |
21 | Oscar Slotosch |
Modelling and Validation: AUTOFOCUS and Quest. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 12(4), pp. 225-227, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
Model checking, Interactive theorem proving, State transition diagrams, Event traces |
21 | Andrew P. Martin |
Relating Z and First-Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 12(3), pp. 199-209, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
Undefinedness, Models, Tools, Theorem proving, Logics, Schemas, Z notation |
21 | Padmanabhan Krishnan |
Consistency checks for UML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APSEC ![In: 7th Asia-Pacific Software Engineering Conference (APSEC 2000), 5-8 December 2000, Singapore, pp. 162-, 2000, IEEE Computer Society, 0-7695-0915-0. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
UML consistency checking, state predicates, PVS theorem prover, Prototype Verification System, partially specified systems, behavioural description, Unified Modeling Language, formal verification, theorem proving, specification languages, diagrams, computation history, UML diagrams, dynamic aspects |
21 | Cynthia Dwork, Moni Naor |
Zaps and Their Applications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 41st Annual Symposium on Foundations of Computer Science, FOCS 2000, 12-14 November 2000, Redondo Beach, California, USA, pp. 283-293, 2000, IEEE Computer Society, 0-7695-0850-2. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
zap, witness-indistinguishable protocol, shared random string model, verifiable pseudo-random bit generators, concurrent deniable authentication, computational complexity, cryptography, NP completeness, theorem proving, public keys, zero-knowledge proofs, verifier, concurrent zero knowledge |
21 | Richard Cleve, John Watrous |
Fast parallel circuits for the quantum Fourier transform. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 41st Annual Symposium on Foundations of Computer Science, FOCS 2000, 12-14 November 2000, Redondo Beach, California, USA, pp. 526-536, 2000, IEEE Computer Society, 0-7695-0850-2. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
fast parallel circuits, quantum Fourier transform, QFT, circuit depth, constant error, depth bound, polynomial size, classical polynomial-time processing, depth complexity, arbitrary modulus, lower bound, theorem proving, quantum computing, Fourier transforms, upper bound, circuit complexity, circuit complexity, quantum circuits, factoring algorithm |
21 | Jeff Kahn 0001, Jeong Han Kim, László Lovász 0001, Van H. Vu |
The Cover Time, the Blanket Time, and the Matthews Bound. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 41st Annual Symposium on Foundations of Computer Science, FOCS 2000, 12-14 November 2000, Redondo Beach, California, USA, pp. 467-475, 2000, IEEE Computer Society, 0-7695-0850-2. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
blanket time, Matthews bound, Matthews bounds, deterministic-polynomial time algorithm, computational complexity, approximation algorithm, graph theory, graph, theorem proving, random walk, deterministic algorithms, approximation theory, stationary distribution, cover time |
21 | Russell A. Martin, Dana Randall |
Sampling Adsorbing Staircase Walks Using a New Markov Chain Decomposition Method. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 41st Annual Symposium on Foundations of Computer Science, FOCS 2000, 12-14 November 2000, Redondo Beach, California, USA, pp. 492-502, 2000, IEEE Computer Society, 0-7695-0850-2. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
adsorbing staircase walks, Markov chain decomposition method, lattice paths, diagonal steps, local Markov chain, /spl lambda//sup /spl kappa//, Gibbs measure, first proof, statistical physics community, Markov chain, theorem proving, Markov processes, lambda calculus, state space, decomposition technique |
21 | John Watrous |
Succinct quantum proofs for properties of finite groups. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 41st Annual Symposium on Foundations of Computer Science, FOCS 2000, 12-14 November 2000, Redondo Beach, California, USA, pp. 537-546, 2000, IEEE Computer Society, 0-7695-0850-2. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
succinct quantum proofs, finite group properties, quantum computational variant, quantum proof, quantum state, NP-type proof, black-box groups, group operations, group oracle, Group Non-Membership problem, bounded error, simple proof, quantum proofs, classical proofs, group properties, computational complexity, theorem proving, quantum computing, quantum computer, certificate, nondeterminism, polynomial time, strings, group theory, finite groups |
21 | Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, Avi Wigderson |
Pseudorandom Generators in Propositional Proof Complexity. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 41st Annual Symposium on Foundations of Computer Science, FOCS 2000, 12-14 November 2000, Redondo Beach, California, USA, pp. 43-53, 2000, IEEE Computer Society, 0-7695-0850-2. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
combinatorial pseudorandom generators, Nisan-Wigderson generator, Tseitin tautologies, polynomial calculus with resolution, polynomial calculus, computational complexity, theorem proving, process algebra, resolution, random processes, pseudorandom generators, propositional proof complexity |
21 | Daniel Brand |
A Software Falsifier. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISSRE ![In: 11th International Symposium on Software Reliability Engineering (ISSRE 2000), 8-11 October 2000, San Jose, CA, USA, pp. 174-185, 2000, IEEE Computer Society, 0-7695-0807-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
static analysis, theorem proving, data-flow analysis, symbolic execution |
Displaying result #401 - #500 of 3383 (100 per page; Change: ) Pages: [ <<][ 1][ 2][ 3][ 4][ 5][ 6][ 7][ 8][ 9][ 10][ 11][ 12][ 13][ 14][ >>] |
|