Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
69 | Shane Sendall, Alfred Strohmeier |
Using OCL and UML to Specify System Behavior. |
Object Modeling with the OCL |
2002 |
DBLP DOI BibTeX RDF |
Pre- and Postcondition Assertions, Unified Modeling Language, Requirements Analysis, Object Constraint Language, Software Specification |
63 | H. B. M. Jonkers |
Upgrading the Pre- and Postcondition Technique. |
VDM Europe (1) |
1991 |
DBLP DOI BibTeX RDF |
|
54 | Shane Sendall, Alfred Strohmeier |
Specifying Concurrent System Behavior and Timing Constraints Using OCL and UML. |
UML |
2001 |
DBLP DOI BibTeX RDF |
Software System Specification, Unified Modeling Language (UML), Concurrent Programming, Timing Constraints, Object Constraint Language (OCL), Pre- and Postcondition |
54 | Frank S. de Boer, Maurizio Gabbrielli, Elena Marchiori, Catuscia Palamidessi |
Proving Concurrent Constraint Programs Correct. |
ACM Trans. Program. Lang. Syst. |
1997 |
DBLP DOI BibTeX RDF |
strongest postcondition, constraint programming, dynamic scheduling, proof theory |
54 | R. Geoff Dromey |
Systematic Program Development. |
IEEE Trans. Software Eng. |
1988 |
DBLP DOI BibTeX RDF |
goal-oriented programming, case analysis, constructive program proofs, software engineering, data structure, refinements, programming, program development, problem decomposition, program structure, postcondition |
45 | Jianxin Li |
Improvements to systematic program development. |
ACM Southeast Regional Conference |
1992 |
DBLP DOI BibTeX RDF |
|
39 | Sumit Gulwani, Saurabh Srivastava 0001, Ramarathnam Venkatesan |
Program analysis as constraint solving. |
PLDI |
2008 |
DBLP DOI BibTeX RDF |
most-general counterexamples, non-termination analysis, strongest postcondition, program verification, constraint solving, weakest precondition, bounds analysis |
39 | Haifeng He, Neelam Gupta |
Automated Debugging Using Path-Based Weakest Preconditions. |
FASE |
2004 |
DBLP DOI BibTeX RDF |
software testing, Fault location, weakest precondition, postcondition |
39 | Aniello Cimitile, Andrea De Lucia, Malcolm Munro |
Identifying reusable functions using specification driven program slicing: a case study. |
ICSM |
1995 |
DBLP DOI BibTeX RDF |
reusable function identification, specification driven program slicing, code fragment isolation, functional abstractions, program statement execution, program predicate execution, entry points, exit points, algorithms, formal specification, software maintenance, software reusability, data flow analysis, symbolic execution, precondition, program diagnostics, dependence graphs, symbol manipulation, control flow graphs, program control structures, C programs, postcondition |
33 | Facundo Molina, Pablo Ponzio, Nazareno Aguirre, Marcelo F. Frias |
EvoSpex: A Search-Based Tool for Postcondition Inference. |
ISSTA |
2023 |
DBLP DOI BibTeX RDF |
|
33 | Hong Lu, Chengyi Wang, Jiacheng Gui, Hao Huang |
PBLInv: Postcondition-based Loop Invariant Learning for C Programs. |
QRS |
2020 |
DBLP DOI BibTeX RDF |
|
33 | Eleanor Davies, Sara Kalvala |
Postcondition-preserving fusion of postorder tree transformations. |
CC |
2020 |
DBLP DOI BibTeX RDF |
|
33 | Daisuke Ishii, Guillaume Melquiond, Shin Nakajima 0001 |
Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus. |
IFM |
2013 |
DBLP DOI BibTeX RDF |
|
33 | Oleh R. Nykyforchyn, Dusan Repovs |
L-fuzzy strongest postcondition predicate transformers as L-idempotent linear or affine operators between semimodules of monotonic predicates. |
Fuzzy Sets Syst. |
2012 |
DBLP DOI BibTeX RDF |
|
33 | Radu Grigore, Julien Charles, Fintan Fairmichael, Joseph Kiniry |
Strongest postcondition of unstructured programs. |
FTfJP@ECOOP |
2009 |
DBLP DOI BibTeX RDF |
|
33 | Gary T. Leavens, Albert L. Baker |
Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. |
World Congress on Formal Methods |
1999 |
DBLP DOI BibTeX RDF |
|
33 | David M. Papurt |
The Sensible Use of Method Overriding: Satisfying Pre- and Postcondition Constraints. |
J. Object Oriented Program. |
1997 |
DBLP BibTeX RDF |
|
33 | Gerald C. Gannod, Betty H. C. Cheng |
Strongest Postcondition Semantics as the Formal Basis for Reverse Engineering. |
Autom. Softw. Eng. |
1996 |
DBLP DOI BibTeX RDF |
|
33 | Gerald C. Gannod, Betty H. C. Cheng |
Strongest Postcondition Semantics as the Formal Basis for Reverse Engineering. |
WCRE |
1995 |
DBLP DOI BibTeX RDF |
|
33 | Ralph-Johan Back, Joakim von Wright |
Statement Inversion and Strongest Postcondition. |
Sci. Comput. Program. |
1993 |
DBLP DOI BibTeX RDF |
|
30 | Karl-Heinz Pennemann |
Development of Correct Graph Transformation Systems. |
ICGT |
2008 |
DBLP DOI BibTeX RDF |
|
30 | Timothy S. Gegg-Harrison |
Constructing contracts: Making discrete mathematics relevant to beginning programmers. |
ACM J. Educ. Resour. Comput. |
2005 |
DBLP DOI BibTeX RDF |
programming by contract, Formal methods, program verification, weakest preconditions, programming tools, loop invariants, axiomatic semantics |
30 | Timothy S. Gegg-Harrison, Gary R. Bunce, Rebecca D. Ganetzky, Christina M. Olson, Joshua D. Wilson |
Studying program correctness in ProVIDE. |
ITiCSE |
2003 |
DBLP DOI BibTeX RDF |
|
30 | Timothy S. Gegg-Harrison, Gary R. Bunce, Rebecca D. Ganetzky, Christina M. Olson, Joshua D. Wilson |
Studying program correctness by constructing contracts. |
ITiCSE |
2003 |
DBLP DOI BibTeX RDF |
Java, design by contract, axiomatic semantics |
30 | Jens Knoop |
Parallel Data-Flow Analysis of Explicitly Parallel Programs. |
Euro-Par |
1999 |
DBLP DOI BibTeX RDF |
|
30 | Gary T. Leavens, Jeannette M. Wing |
Protective Interface Specifications. |
TAPSOFT |
1997 |
DBLP DOI BibTeX RDF |
|
30 | Alexander Borgida, John Mylopoulos, Raymond Reiter |
On the Frame Problem in Procedure Specifications. |
IEEE Trans. Software Eng. |
1995 |
DBLP DOI BibTeX RDF |
frame assertion, semantics of specification languages, specifications, languages, inheritance, Formal, proof obligations |
30 | Frank S. de Boer, Maurizio Gabbrielli, Elena Marchiori, Catuscia Palamidessi |
Proving Concurrent Constraint Programs Correct. |
POPL |
1994 |
DBLP DOI BibTeX RDF |
|
30 | Gerald Futschek |
Algebraic Properties of Loop Invariants. |
Formal Methods in Programming and Their Applications |
1993 |
DBLP DOI BibTeX RDF |
|
30 | Andrzej Blikle |
Assertion Programming. |
MFCS |
1979 |
DBLP DOI BibTeX RDF |
|
24 | Michael Greenberg 0002, Benjamin C. Pierce, Stephanie Weirich |
Contracts made manifest. |
POPL |
2010 |
DBLP DOI BibTeX RDF |
blame, dynamic checking, refinement type, contract, translation, precondition, postcondition |
24 | Raymond T. Boute |
Calculational semantics: Deriving programming theories from equations by functional predicate calculus. |
ACM Trans. Program. Lang. Syst. |
2006 |
DBLP DOI BibTeX RDF |
calculational reasoning, functional predicate calculus, intuitive semantics, strongest postcondition, weakest antecondition, termination, formal semantics, programming theories, Assignment, generic functionals, loops, nondeterminacy, axiomatic semantics |
24 | Dana N. Xu |
Extended static checking for haskell. |
Haskell |
2006 |
DBLP DOI BibTeX RDF |
counterexample guided unrolling, pre/postcondition, symbolic simplification |
24 | Martin Gogolla, Jörn Bohling, Mark Richters |
Validating UML and OCL models in USE by automatic snapshot generation. |
Softw. Syst. Model. |
2005 |
DBLP DOI BibTeX RDF |
models, UML, Invariant, Reasoning, OCL, Test case, Class diagram, Model validation, Snapshot, Pre- and postcondition, Model testing |
24 | Martin Blom, Eivind J. Nordby, Anna Brunström |
An Experimental Evaluation of Programming by Contract. |
ECBS |
2002 |
DBLP DOI BibTeX RDF |
evaluation, Experiment, contract, precondition, postcondition |
24 | Andreas Blass, Yuri Gurevich |
Inadequacy of computable loop invariants. |
ACM Trans. Comput. Log. |
2001 |
DBLP DOI BibTeX RDF |
postcondition uncomputable, recursive inseparability, assertion, automated reasoning, precondition, Hoare logic, automated deduction, loop invariants |
24 | In Sang Chung, Wan Kwon Lee, Gwang Sik Yoon, Yong Rae Kwon |
Program slicing based on specification. |
SAC |
2001 |
DBLP DOI BibTeX RDF |
strongest postcondition, software maintenance, software reuse, program slice, weakest precondition |
15 | Jordi Cabot, Robert Clarisó, Daniel Riera |
Verifying UML/OCL Operation Contracts. |
IFM |
2009 |
DBLP DOI BibTeX RDF |
|
15 | Ming Fu, Yu Zhang 0086, Yong Li |
Formal Reasoning about Concurrent Assembly Code with Reentrant Locks. |
TASE |
2009 |
DBLP DOI BibTeX RDF |
|
15 | Dan Li, Xiaoshan Li, Jicong Liu, Zhiming Liu 0001 |
Validation of requirement models by automatic prototyping. |
Innov. Syst. Softw. Eng. |
2008 |
DBLP DOI BibTeX RDF |
UML, Prototype, Code generation, OCL, Requirement validation |
15 | Yogesh Singh, Anju Saha |
Enhancing Data Flow Testing of Classes through Design by Contract. |
ACIS-ICIS |
2008 |
DBLP DOI BibTeX RDF |
design by contract, object oriented testing, data flow testing |
15 | Naoyasu Ubayashi, Jinji Piao, Suguru Shinotsuka, Tetsuo Tamai |
Contract-Based Verification for Aspect-Oriented Refactoring. |
ICST |
2008 |
DBLP DOI BibTeX RDF |
Verification, AOP, Refactoring, Contract |
15 | Wladimir Araujo, Lionel C. Briand, Yvan Labiche |
Concurrent Contracts for Java in JML. |
ISSRE |
2008 |
DBLP DOI BibTeX RDF |
|
15 | Karl Azab, Annegret Habel |
High-Level Programs and Program Conditions. |
ICGT |
2008 |
DBLP DOI BibTeX RDF |
|
15 | Yoonsik Cheon, Ashaveena Perumandla |
Specifying and checking method call sequences of Java programs. |
Softw. Qual. J. |
2007 |
DBLP DOI BibTeX RDF |
Method call sequence specification, Programming by contract, Assertion, Pre and postconditions, Runtime checking, JML language |
15 | Torben Amtoft, Anindya Banerjee 0001 |
Verification condition generation for conditional information flow. |
FMSE |
2007 |
DBLP DOI BibTeX RDF |
conditional information flow analysis, object invariants, verification condition generation |
15 | Steve M. Shaner, Gary T. Leavens, David A. Naumann |
Modular verification of higher-order methods with mandatory calls specified by model programs. |
OOPSLA |
2007 |
DBLP DOI BibTeX RDF |
grey-box approach, higher order method, mandatory call, model program, verification, specification languages, hoare logic, refinement calculus |
15 | Sumit Gulwani, Nebojsa Jojic |
Program verification as probabilistic inference. |
POPL |
2007 |
DBLP DOI BibTeX RDF |
automated recovery machine, forward and backward analysis, over and under approximation, learning, program verification, Markov chain Monte Carlo, Gibbs sampling, belief networks, probabilistic inference, factor graphs |
15 | Kenneth L. Knowles, Cormac Flanagan |
Type Reconstruction for General Refinement Types. |
ESOP |
2007 |
DBLP DOI BibTeX RDF |
|
15 | Ingrid Rewitzky, Chris Brink |
Monotone Predicate Transformers as Up-Closed Multirelations. |
RelMiCS |
2006 |
DBLP DOI BibTeX RDF |
|
15 | Torben Amtoft, Sruthi Bandhakavi, Anindya Banerjee 0001 |
A logic for information flow in object-oriented programs. |
POPL |
2006 |
DBLP DOI BibTeX RDF |
information flow, confidentiality, aliasing |
15 | Chetan Shiva Shankar, Roy H. Campbell |
Ordering Management Actions in Pervasive Systems using Specification-enhanced Policies. |
PerCom |
2006 |
DBLP DOI BibTeX RDF |
|
15 | Joxan Jaffar, Andrew E. Santosa, Razvan Voicu |
A CLP Method for Compositional and Intermittent Predicate Abstraction. |
VMCAI |
2006 |
DBLP DOI BibTeX RDF |
|
15 | Yishai A. Feldman, Leon Gendler |
Discern: Towards the Automatic Discovery of Software Contracts. |
SEFM |
2006 |
DBLP DOI BibTeX RDF |
|
15 | Robert Glück, Masahiko Kawabe |
Revisiting an automatic program inverter for Lisp. |
ACM SIGPLAN Notices |
2005 |
DBLP DOI BibTeX RDF |
LISP |
15 | Chetan Shiva Shankar, Roy H. Campbell |
A Policy-based Management Framework for Pervasive Systems using Axiomatized Rule-Actions. |
NCA |
2005 |
DBLP DOI BibTeX RDF |
|
15 | Wojciech J. Dzidek, Lionel C. Briand, Yvan Labiche |
Lessons Learned from Developing a Dynamic OCL Constraint Enforcement Tool for Java. |
MoDELS (Satellite Events) |
2005 |
DBLP DOI BibTeX RDF |
|
15 | Frank Zeyda, Bill Stoddart, Steve Dunne |
A Prospective-Value Semantics for the GSL. |
ZB |
2005 |
DBLP DOI BibTeX RDF |
bunch theory, prospective-value semantics, expression transformers, wp calculus, B Method, Generalised substitution |
15 | Bernhard K. Aichernig, Percy Antonio Pari Salas |
Test Case Generation by OCL Mutation and Constraint Solving. |
QSIC |
2005 |
DBLP DOI BibTeX RDF |
|
15 | Sarfraz Khurshid, Darko Marinov |
TestEra: Specification-Based Testing of Java Programs Using SAT. |
Autom. Softw. Eng. |
2004 |
DBLP DOI BibTeX RDF |
Java testing, TestEra, SAT enumeration, software testing, specification-based testing, Alloy, automated test generation |
15 | Ziyang Duan, Arthur J. Bernstein, Philip M. Lewis, Shiyong Lu |
Semantics Based Verification and Synthesis of BPEL4WS Abstract Processes. |
ICWS |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Jim Woodcock 0001, Ana Cavalcanti 0001 |
A Tutorial Introduction to Designs in Unifying Theories of Programming. |
IFM |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Michael Poppleton, Richard Banach |
Requirements Validation by Lifting Retrenchments in B. |
ICECCS |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Orieta Celiku, Joakim von Wright |
Implementing Angelic Nondeterminism. |
APSEC |
2003 |
DBLP DOI BibTeX RDF |
|
15 | Kinh Nguyen, Tharam S. Dillon |
Atomic Use Case: A Concept for Precise Modelling of Object-Oriented Information Systems. |
OOIS |
2003 |
DBLP DOI BibTeX RDF |
|
15 | Frank D. Valencia |
Timed Concurrent Constraint Programming: Decidability Results and Their Application to LTL. |
ICLP |
2003 |
DBLP DOI BibTeX RDF |
|
15 | Orieta Celiku, Joakim von Wright |
Theorem Prover Support for Precondition and Correctness Calculation. |
ICFEM |
2002 |
DBLP DOI BibTeX RDF |
|
15 | Colin J. Fidge |
Timing Analysis of Assembler Code Control-Flow Paths. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
15 | Alain Couchot |
Improving the Refined Triggering Graph Method for Active Rules Termination Analysis. |
BNCOD |
2002 |
DBLP DOI BibTeX RDF |
|
15 | Scott M. Pike, Nigamanth Sridhar |
Early-Reply Components: Concurrent Execution with Sequential Reasoning. |
ICSR |
2002 |
DBLP DOI BibTeX RDF |
|
15 | Chandrasekhar Boyapati, Sarfraz Khurshid, Darko Marinov |
Korat: automated testing based on Java predicates. |
ISSTA |
2002 |
DBLP DOI BibTeX RDF |
|
15 | Lionel C. Briand, Yvan Labiche, Hong Sun |
Investigating the use of analysis contracts to support fault isolation in object oriented code. |
ISSTA |
2002 |
DBLP DOI BibTeX RDF |
contracts, testability, object-oriented analysis, object-oriented testing |
15 | Heinz W. Schmidt, Bernd J. Krämer, Iman Poernomo, Ralf H. Reussner |
Predictable Component Architectures Using Dependent Finite State Machines. |
RISSEF |
2002 |
DBLP DOI BibTeX RDF |
automated interface adaptation, component-based interface specification, component-based prediction, production cell, protocol types, parameterised contracts, software architecture, finite state machines |
15 | Rafael Ceballos, Rafael M. Gasca, Carmelo Del Valle, Miguel Toro |
Max-CSP Approach for Software Diagnosis. |
IBERAMIA |
2002 |
DBLP DOI BibTeX RDF |
|
15 | Pierre Metz, John O'Brien, Wolfgang Weber 0006 |
Against Use Case Interleaving. |
UML |
2001 |
DBLP DOI BibTeX RDF |
|
15 | Claus Pahl |
Components, Contracts, and Connectors for the Unified Modelling Language UML. |
FME |
2001 |
DBLP DOI BibTeX RDF |
|
15 | Catuscia Palamidessi, Frank D. Valencia |
A Temporal Concurrent Constraint Programming Calculus. |
CP |
2001 |
DBLP DOI BibTeX RDF |
|
15 | Pedro Guerreiro |
Simple Support for Design by Contract in C++. |
TOOLS (39) |
2001 |
DBLP DOI BibTeX RDF |
|
15 | Roope Kaivola, Mark D. Aagaard |
Divider Circuit Verification with Model Checking and Theorem Proving. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
15 | Andreas Nonnengart |
Hybrid Systems Verification by Location Elimination. |
HSCC |
2000 |
DBLP DOI BibTeX RDF |
|
15 | Marc Shapiro 0001, Antony I. T. Rowstron, Anne-Marie Kermarrec |
Application-independent reconciliation for nomadic applications. |
ACM SIGOPS European Workshop |
2000 |
DBLP DOI BibTeX RDF |
|
15 | Patrick Doherty 0001, Witold Lukaszewicz, Ewa Madalinska-Bugaj |
Computing MPMA Updates Using Dijkstra's Semantics. |
ISMIS |
1999 |
DBLP DOI BibTeX RDF |
|
15 | Yoonsik Cheon, Heung-Nam Kim |
Sequence Operators: Specifying Behavioral Interfaces of Smalltalk Blocks. |
APSEC |
1999 |
DBLP DOI BibTeX RDF |
sequence operator, specification language, Smalltalk, formal semantics, block, Program specification |
15 | Raphaël Couturier, Dominique Méry |
An Experiment in Parallelizing an Application Using Formal Methods. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
15 | Susanne Graf, Hassen Saïdi |
Construction of Abstract State Graphs with PVS. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
state graph exploration, theorem proving, abstract interpretation |
15 | Gerald C. Gannod, Betty H. C. Cheng |
A Formal Automated Approach for Reverse Engineering Programs with Pointers. |
ASE |
1997 |
DBLP DOI BibTeX RDF |
reverse engineering programs, formal automated approach, formal specification, formal specifications, reverse engineering, programming language, formal semantics, pointers |
15 | Victor Carreño |
Verification in Higher Order Logic of Mutual Exclusion Algorithm. |
HUG |
1993 |
DBLP DOI BibTeX RDF |
|
15 | Wim H. Hesselink, Ronald Reinds |
Temporal Preconditions of Recursive Procedures. |
REX Workshop |
1992 |
DBLP DOI BibTeX RDF |
leads-to, eventually, healthiness law, guarded recursion, unfolding, weakest precondition, recursive procedure |
15 | Jozef Hooman |
Compositional Verification of Real-Time Systems using Extended Hoare Triples. |
REX Workshop |
1991 |
DBLP DOI BibTeX RDF |
Hoare triples, Verification, Real-time, Specification, Compositionality |
15 | Hans-Juergen Boehm |
Side Effects and Aliasing Can Have Simple Axiomatic Descriptions. |
ACM Trans. Program. Lang. Syst. |
1985 |
DBLP DOI BibTeX RDF |
|
15 | Theo M. V. Janssen, Peter van Emde Boas |
On the Proper Treatment or Referencing, Dereferencing and Assignment. |
ICALP |
1977 |
DBLP DOI BibTeX RDF |
|