Research - Impact
Some statistics regarding publications of Jan Jürjens
In Jan. 2015, a search delivered more than 4000 citations of my publications at Google Scholar, with an h-index 33. According to
the Google Scholar citations, my most highly-used research outputs include the UMLsec research monograph (more than 700
citations according to Google Scholar) and the conference papers at UML'02 (more than 500 citations; Ten
Year Most Influential Paper Award of the conference ``Models 2012''), TACS'01 (more than 150 citations, among
the 6 most cited TACS article, and the 2nd-most cited TACS'01 paper according to Google Scholar (on 7.10.2012)) and FASE'01 (more than 150 citations, among
the 5 most cited FASE articles, and the most cited FASE'01 paper according to Google Scholar (on 7.10.2012)).
See also my DBLP publication list (which lists me as one of roughly 4000 most prolific DBLP
authors - whatever that means...).
Relevant overviews from other sources
Model-Driven Security is considered an important emerging technology in the following Gartner report: Gartner
Briefing G00151498, Model-Driven Security:
Enabling a Real-Time, Adaptive Security Infrastructure, 21st September 2007
Wikipedia entry on Model-Driven
Security.
Nice overview on Software Engineering for Secure Software: K. R. Jayaram and Aditya Mathur, Software Engineering for Secure Software - State of
the Art: A Survey. August 2005.Technical Report CERIAS-TR-2005-67, SERC-TR-279
Interesting industrial application of secure software engineering: Axelle Apvrille, Makan Pourzandi: Secure Software Development by Example. IEEE Security & Privacy 3(4): 10-17 (2005)
Relevant article in the Build
Security In body of knowledge: Samuel T. Redwine:
Introduction to Modeling Tools for Software Security
, 2007
Overview on Software Assurance by Sam Redwine.
State of the art regarding secure software development in practice today, with some recommendations how to improve
on that: Bill Whyte and John Harrison:
Secure Software Development - a White Paper
, 2008
Suggestions for future research in secure software engineering: Martin Wirsing: Software Engineering for Secure Software-Intensive Systems, Consultation meeting on "Engineering Secure
Software Systems" in the context of the preparation of the EU FP7 ICT work programme 2009-2010.
Who is Who's
Descriptions of impact for selected publications
- Jan Jürjens, Secure Systems Development with UML, © Springer-Verlag,
Heidelberg, 2005. 300 pages.
Chinese translation: Tsinghua University Press, Beijing 2009
(Submitted to the nationwide Research Assessment Exercise (RAE), UK 2008)
First book on model-based security engineering with UML (a field which was initiated by the author`s FASE`01
paper). Includes the first security extension of UML, its formal foundations, and applications for example to a
smart-card based payment system developed by Visa International. The article led to work by the author on automated
formal verification of UMLsec models (for which the verification technique was presented at ICSE`05, and tools for
it at ICSE`06) and applications at BMW (ICSE`07), O2 (Germany) (ICSE`08) and other companies. Led to keynotes
(SECRYPT`06, Software Engineering`07), projects totalling 5 Mio EUR using UMLsec, a series of PhD theses and about
100 related journal and conference papers co-authored by the author totalling over 3000 citations at Google Scholar
in 2012.
@BOOK{UMLsecBook05,
title = {Secure Systems Development with {UML}},
publisher = {Springer},
year = {2005},
author = {J.~{J}{\"u}{r}jens},
pages = {300},
doi = {http://dx.doi.org/10.1007/b137706},
note = {Chinese translation: Tsinghua University Press, Beijing 2009},
keywords = {selectedPub,book,vorsecurestreams}
}
[Show
BibTex] [ DOI ]
- A. Bauer, J. Jürjens, Yijun Yu. Runtime Security Traceability for Evolving Systems. The Computer Journal,
Oxford Univ. Press, 54/1, 2011, pp. 58-87.
Security-critical systems are challenging to design and implement correctly and securely. A lot of
vulnerabilities have been found in current software systems both at the specification and the implementation
levels. This paper presents a comprehensive approach for model-based security assurance. Initially, it allows one
to formally verify the design models against high-level security requirements such as secrecy and authentication on
the specification level, and helps to ensure that their implementation adheres to these properties, if they express
a system's run-time behaviour. As such, it provides a traceability link from the design model to its implementation
by which the actual system can then be verified against the model while it executes. This part of our approach
relies on a technique also known as run-time verification. The extra effort for it is small as most of the
computation is automated; however, additional resources at run-time may be required. If during run-time
verification a security weakness is uncovered, it can be removed using aspect- oriented security hardening
transformations. Therefore, this approach also supports the evolution of software since the traceability mapping is
updated when refactoring operations are regressively performed using our tool-supported refactoring technique. The
proposed method has been applied to the Java-based implementation JESSIE of the Internet security protocol SSL, in
which a security weakness was detected and fixed using our approach. We also explain how the traceability link can
be transformed to the official implementation of the Java Secure Sockets Extension (J SSE) that was recently made
open source by Sun.
- S.H. Houmb, S. Islam, E. Knauss, J. Jürjens, K. Schneider. Eliciting Security Requirements and Tracing them to
Design: An Integration of Common Criteria, Heuristics, and UMLsec. Requirements Engineering Journal (REJ),
Springer-Verlag, vol. 15, no. 1, pp. 63-93, 2010.
Building secure systems is difficult for many reasons. This paper deals with two of the main challenges: (i) the
lack of security expertise in development teams, and (ii) the inadequacy of existing methodologies to support
developers who are not security experts. The security standard ISO 14508 (Common Criteria) together with secure
design techniques such as UMLsec can provide the security expertise, knowledge, and guidelines that are needed.
However, security expertise and guidelines are not stated explicitly in the Common Criteria. They are rather
phrased in security domain terminology and difficult to understand for developers. This means that some general
security and secure design expertise are required to fully take advantage of the Common Criteria and UMLsec. In
addition, there is the problem of tracing security requirements and objectives into solution design, which is
needed for proof of requirements fulfilment. This paper describes a security requirements engineering methodology
called SecReq. SecReq combines three techniques: the Common Criteria, the heuristic requirements ed- itor HeRA, and
UMLsec. SecReq makes systematic use of the security engineering knowledge contained in the Common Criteria and
UMLsec, as well as security-related heuristics in the HeRA tool. The integrated SecReq method supports early
detection of security-related issues (HeRA), their systematic refinement guided by the Common Criteria, and the
ability to trace security requirements into UML design models. A feedback loop helps reusing experience within
SecReq and turns the approach into an iterative process for the secure system life-cycle, also in the presence of
system evolution.
@ARTICLE{rej10HIKJS,
author = {S.H.~Houmb and S.~Islam and E.~Knauss and J.~{J}{\"u}{r}jens and
K.~Schneider},
title = {Eliciting Security Requirements and Tracing them to Design: An Integration
of {Common Criteria, Heuristics, and UMLsec}},
journal = {Requirements Engineering Journal (REJ), Springer-Verlag},
year = {2010},
volume = {15},
pages = {63--93},
number = {1},
note = {Special issue on Security Requirements Engineering},
file = {preprint:http\://rgse.uni-koblenz.de/jj/publications/papers/JRE_SR_Elicitation.pdf:URL},
keywords = {selectedPub,modelbasedSecurityEngineering}
}
[Show
BibTex] [ preprint ]
- J. Jürjens. A Domain-Specific Language for Cryptographic Protocols based on Streams. Journal of Logic and
Algebraic Programming (JLAP), vol. 78, Jan./Feb. 2009, pp. 54-73.
Developing security-critical systems is difficult and there are many well-known examples of security weaknesses
exploited in practice. Thus a sound methodology supporting secure systems development is urgently needed. In
particular, an important missing link in the construction of secure systems is finding a practical way to create
reliably secure crypto protocol implementations. We present an approach that aims to address this need by making
use of a domain-specific language for crypto protocol implementations. One can use this language to construct a
compact and precise yet executable representation of a cryptographic protocol. This high-level program can be
verified against the security goals using automated theorem provers for first order logic. One can then use it to
provide assurance for legacy implementations of crypto protocols by generating test-cases.
[Show
Abstract]
@ARTICLE{jlap09J,
author = {J.~{J}{\"u}{r}jens},
title = {A domain-specific language for cryptographic protocols based on streams},
journal = {Journal of Logic and Algebraic Programming},
year = {2009},
volume = {78},
pages = {54--73},
number = {2},
month = {January - February},
abstract = {Developing security-critical systems is difficult and there are many
well-known examples of security weaknesses exploited in practice.
Thus a sound methodology supporting secure systems development is
urgently needed. In particular, an important missing link in the
construction of secure systems is finding a practical way to create
reliably secure crypto protocol implementations. We present an approach
that aims to address this need by making use of a domain-specific
language for crypto protocol implementations. One can use this language
to construct a compact and precise yet executable representation
of a cryptographic protocol. This high-level program can be verified
against the security goals using automated theorem provers for first
order logic. One can then use it to provide assurance for legacy
implementations of crypto protocols by generating test-cases.},
doi = {http://dx.doi.org/10.1016/j.jlap.2008.08.006},
file = {preprint:http\://rgse.uni-koblenz.de/jj/publications/papers/jlap07.pdf:URL},
keywords = {selectedPub,modelbasedSecurityEngineering,vorsecurestreams}
}
[Show
BibTex] [ DOI ] [ preprint ]
- M. Aizatulin, A.D. Gordon, J. Jürjens. Computational Verification of C Protocol Implementations by Symbolic
Execution. 19th ACM Conference on Computer and Communications Security (CCS 2012), ACM 2012.
We verify cryptographic protocols coded in C for correspondence properties with respect to the computational
model of cryptography. Our first step uses symbolic execution to extract a process calculus model from a C
implementation of the protocol. The new contribution is the second step in which we translate the extracted model
to a CryptoVerif protocol description, such that successful verification with CryptoVerif implies the security of
the original C implementation. We implement our method and apply it to verify several protocols out of reach of
previous work in the symbolic model (using ProVerif), either due to the use of XOR and Diffie-Hellman commitments,
or due to the lack of an appropriate computational soundness result. We analyse only a single execution path, so
our tool is limited to code following a fixed protocol narration. This is the first security analysis of C code to
target a verifier for the computational model. We successfully verify over 3000 LOC. One example (about 1000 LOC)
is independently written and currently in testing phase for industrial deployment; during its analysis we uncovered
a vulnerability now fixed by its author.
@INPROCEEDINGS{ccs12AGJ,
author = {M.~Aizatulin and A.D.~Gordon and J.~J{\"u}rjens},
title = {Computational Verification of C Protocol Implementations by Symbolic
Execution},
booktitle = {19th ACM Conference on Computer and Communications Security (CCS
2012)},
year = {2012},
pages = {712--723},
doi = {http://doi.acm.org/10.1145/2382196.2382271},
publisher = {ACM},
file =
{slides:http\://rgse.uni-koblenz.de/secse/pages/people/juerjens/publications/slides/ccs12AGJslides.pdf:URL;paper:http\://rgse.uni-koblenz.de/secse/pages/people/juerjens/publications/papers/ccs12AGJ.pdf:URL},
keywords = {selectedPub,secureSoftwareEngineeringCodeSecurityAnalysis,vorsecurestreams}
}
[Show
BibTex] [ DOI ] [ slides ] [
paper ]
- F. Dupressoir, A.D. Gordon, J. Jürjens, D. Naumann. Guiding a General-Purpose C Verifier to Prove
Cryptographic Protocols. 24th IEEE Computer Security Foundations Symposium (CSF 2011), IEEE 2011, pp. 3-17.
We describe how to verify security properties of C code for cryptographic protocols by using a general-purpose
verifier. We prove security theorems in the symbolic model of cryptography. Our techniques include: use of ghost
state to attach formal algebraic terms to concrete byte arrays and to detect collisions when two distinct terms map
to the same byte array; decoration of a crypto API with contracts based on symbolic terms; and expression of the
attacker model in terms of C programs. We rely on the general-purpose verifier VCC; we guide VCC to prove security
simply by writing suitable header files and annotations in implementation files, rather than by changing VCC
itself. We formalize the symbolic model in Coq in order to justify the addition of axioms to VCC.
@Article{DGJN14,
author = {F.~Dupressoir and A.D.~Gordon and J.~J\"urjens and D.~Naumann},
title = {Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols},
journal = {Journal of Computer Security},
volume = {22},
number = {5},
pages = {823--866},
year = {2014},
note = {Special issue with best papers from the 24th IEEE Computer Security Foundations Symposium (CSF)},
file = {preprint:http\://arxiv.org/abs/1312.6532:URL},
keywords = {selectedPub,hotOffThePress, modelbasedSecurityEngineering}
}
[Show
BibTex] [ preprint ]
- J. Jürjens. Security Analysis of Crypto-based Java Programs using Automated Theorem Provers. In 21st
International Conference on Automated Software Engineering (ASE 2006), IEEE/ACM, 2006, pages 167-176.
(Submitted to the nationwide Research Assessment Exercise (RAE), UK 2008)
First formal verification of crypto-protocol legacy implementations for high-level data security requirements.
Provides first solution to open problem of insecure crypto-protocol Java implementations (with respect to the
Dolev-Yao adversary model) which present security threat to e-commerce applications, which are usually used over
computer networks secured by crypto-protocols. Led to first-of-a-kind application to a biometric authentication
protocol developed by a large telecommunications company which uncovered three ma jor security flaws regarding a
novel kind of attack that were then fixed (ACSAC`05).
[Show
Abstract]
@INPROCEEDINGS{sacbjp06,
author = {J.~{J}{\"u}{r}jens},
title = {Security Analysis of Crypto-based Java Programs using Automated Theorem
Provers},
booktitle = {21st IEEE/ACM International Conference on Automated Software Engineering
(ASE 2006)},
year = {2006},
editor = {S.~Easterbrook and S.~Uchitel},
pages = {167-176},
publisher = {ACM},
abstract = {Determining the security properties satisfied by software using cryptography
is difficult: Security requirements such as secrecy, integrity and
authenticity of data are notoriously hard to establish, especially
in the context of cryptographic interactions. Nevertheless, little
attention has been paid so far to the verification of such implementations
with respect to the secure use of cryptography. We propose an approach
to use automated theorem provers for first-order logic to formally
verify crypto-based Java implementations, based on control flow graphs.
It supports an abstract and modular security analysis by using assertions
in the source code. Thus large software systems can be divided into
small parts for which a formal security analysis can be performed
more easily and the results composed. The assertions are validated
against the program behavior in a run-time analysis. Our approach
is supported by the tool JavaSec available as open-source and validated
in an application to a Java Card implementation of the Common Electronic
Purse Specifications and the Java implementation Jessie of SSL.},
doi = {http://dx.doi.org/10.1109/ASE.2006.60},
file =
{slides:http\://rgse.uni-koblenz.de/jj/publications/papers/ase06talk.pdf:URL;paper:http\://rgse.uni-koblenz.de/jj/publications/papers/ase06.pdf:URL},
keywords = {secureSoftwareEngineeringCodeSecurityAnalysis}
}
[Show
BibTex] [ DOI ] [ slides ] [ paper ]
- J. Jürjens, Sound Methods and Effective Tools for Model-based Security Engineering with UML, 27th
International Conference on Software Engineering (ICSE), ACM, 2005, pages 322-331.
This article provides formally based, automated verification tool-support for the security extension of UML
defined in earlier work. It thus prepares the way for the results in the area of model-based development of secure
systems to be used in a formally sound but automated way by practitioners in industry who may be neither security
nor formal methods experts. The tools have subsequently been successfully used in industry to analyze
security-critical systems for vulnerabilities and to correctly design new secure systems. The article presents a
general tool-suite for formal analysis of UML models, explains one such analysis plug-in based on automated theorem
provers for first-order logic in more detail, and demonstrates usefulness at the hand of several industrial
case-studies.
[Show
BibTex] [ slides
] [ paper ]
- J. Jürjens, UMLsec: Extending UML for Secure Systems Development, 5th International Conference on The
Unified Modeling Language (UML 2002), volume 2460 of Lecture Notes in Computer Science, Springer, 2002, pages
412-425. © Springer-Verlag
Ten Year Most Influential Paper of UML 2002
Based on an earlier article by the same author at FASE`01, this article is the first major article in the area
of model-based development of secure systems, of which the author is one of the main founders. This field is
attracting quickly increasing attention, with several workshops devoted to the topics over the last few years. It
also has a significant impact in industry, where it has been successfully used to analyze security-critical systems
for vulnerabilities and to correctly design new secure systems. The article defines an extension of UML for secure
systems design and demonstrates usefulness at the hand of several case-studies.
@INPROCEEDINGS{uml02J,
author = {J.~{J}{\"u}{r}jens},
title = {{UMLsec}: Extending {UML} for Secure Systems Development},
booktitle = {5th International Conference on the Unified Modeling Language (UML
2002)},
year = {2002},
volume = {2460},
series = {Lecture Notes in Computer Science},
pages = {412--425},
publisher = {Springer Verlag},
note = {10 years most influential paper award at Models 2012},
file = {slides:http\://rgse.uni-koblenz.de/jj/publications/papers/uml02talk.pdf:URL;paper
(pdf):http\://rgse.uni-koblenz.de/jj/publications/papers/uml02.pdf:URL;paper
(ps):http\://rgse.uni-koblenz.de/jj/publications/papers/uml02.ps:URL},
keywords = {secureSoftwareEngineeringUMLsecProfile}
}
[Show
BibTex] [ slides
] [ paper (pdf) ] [
paper (ps) ]
- M. Abadi and J. Jürjens, Formal Eavesdropping and its Computational Interpretation, Theoretical Aspects of
Computer Software (4th International Symposium, TACS 2001), volume 2215 of Lecture Notes in Computer Science,
Springer, 2001, pages 82-94. ©
Springer-Verlag
(Submitted to the nationwide Research Assessment Exercise (RAE), UK 2008)
Based on a conference article by Abadi and Rogaway (2000), the current paper was the first to deliver a
soundness result for symbolic crypto-protocol modelling of complete protocol executions against
complexity-theoretical models, and in particular one of the first in a new line of research in formal verification
of crypto-protocols. Addresses the question how common symbolic verification models for crypto protocols relate to
the more fine-grained complexity-theoretical models used in the cryptography community. Triggered by these two
articles over 20 research groups now work on related problems, including groups at Microsoft Research, IBM/Zurich,
MIT, Stanford, and Ecole Normale Superieure
.
[Show
Abstract]
@INPROCEEDINGS{feci01,
author = {M.~Abadi and J.~{J}{\"u}{r}jens},
title = {Formal Eavesdropping and its Computational Interpretation},
booktitle = {Theoretical Aspects of Computer Software (4th International Symposium,
TACS 2001)},
year = {2001},
editor = {N. Kobayashi and {B. C.} Pierce},
volume = {2215},
series = {Lecture Notes in Computer Science},
pages = {82--94},
publisher = {Springer Verlag},
abstract = {We compare two views of symmetric cryptographic primitives in the
context of the systems that use them. We express those systems in
a smple programming language; each if the views yields a semantics
for the language. On of the semantics treats cryptographic operations
formally (that is, symbolically). The other semantics is more detailed
on bitstrings. Each semantics leads to a definition of equivalence
of systems with respect to eavesdroppers. We establish the soundness
of the formal definition with respect to the computational one. This
result provides a precise computational justification for formal
reasoning about security against eavesdroppers.},
doi = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.1076},
file = {extended version:http\://rgse.uni-koblenz.de/jj/publications/papers/lambdaweb.pdf:URL;(older)
slides:http\://rgse.uni-koblenz.de/jj/publications/papers/dagstuhl.ps:URL;paper
(pdf):http\://rgse.uni-koblenz.de/jj/publications/papers/lambda.pdf:URL;paper
(ps):http\://rgse.uni-koblenz.de/jj/publications/papers/lambda.ps:URL},
keywords = {secureSoftwareEngineeringFoundationsOfSecurity}
}
[Show
BibTex] [ DOI ] [
extended version ] [
(older) slides ] [
paper (pdf) ] [
paper (ps) ]
- J. Jürjens, Secrecy-preserving Refinement, International Symposium on Formal Methods Europe (FME 2001),
volume 2021 of Lecture Notes in Computer Science, Springer, 2001, pages 135-152. © Springer-Verlag
This article proposes a solution for an open problem in the area of formal verification of security-critical
systems, namely the so-called "refinement paradox", which means that in many approaches to formal verification of
security, security requirements are not preserved by refinement. This is very unfortunate, since it forces one to
redo the verification after each refinement step, and dangerous, because the implemented system will always be a
refinement even of the most detailed model. The article solves this problem by presenting a formal approach where
important security requirements (formalized in a classical Dolev-Yao style way) are indeed preserved by the
standard refinement operator. This is achieved by separating non-determinism in the sense of underspecification
from run-time nondeterminism (unpredictability) needed for security functionality.
[Show
Abstract]
@INPROCEEDINGS{spr01,
author = {J.~{J}{\"u}{r}jens},
title = {Secrecy-preserving Refinement},
booktitle = {International Symposium on Formal Methods Europe (FME)},
year = {2001},
editor = {J. Fiadeiro and P. Zave},
volume = {2021},
series = {Lecture Notes in Computer Science},
pages = {135-152},
address = {Berlin Heidelberg New York},
publisher = {Springer Verlag},
abstract = {A useful paradigm of system development is that of stepwise refinement.
In contrast to other system properties, many security properties
proposed in the literature are not preserved under refinement (refinement
paradox). We present work towards a framework for stepwise development
of secure systems by showing a notion of secrecy (that follows a
standard approach) to be preserved by standard refinement operators
in the specification framework Focus (extended with cryptographic
primitives). We also give a rely/guarantee version of the secrecy
property and show preservation by refinement. We use the secrecy
property to uncover a previously unpublished flaw in a proposed variant
of TLS, propose a correction and prove it secure. We give an abstract
specification of a secure channel satisfying secrecy and refine it
to a more concrete specification that by the preservation result
thus also satisfies secrecy.},
doi = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.11},
file = {slides:http\://rgse.uni-koblenz.de/jj/publications/papers/J00kSli.pdf:URL;paper
(ps):http\://rgse.uni-koblenz.de/jj/publications/papers/J00kWeb.ps:URL;paper
(pdf):http\://rgse.uni-koblenz.de/jj/publications/papers/J00kWeb.pdf:URL},
keywords = {secureSoftwareEngineeringFoundationsOfSecurity},
summary = {Presents secrecy property preserved under refinement; uncovers flaw
in variant of security protocol TLS.}
}
[Show
BibTex] [ DOI ] [
slides ] [ paper (ps) ] [ paper (pdf) ]
- Jan Jürjens, On a problem of Gabriel and Ulmer, Journal of Pure and Applied Algebra, vol. 158 (2001), pp.
183–196. © Elsevier.
(Submitted to the nationwide Research Assessment Exercise (RAE), UK 2008)
Solved open problem in locally presentable categories from classic book by Gabriel, Ulmer (1971) on
characterisations of models for Horn formulas. Solution refuted classification theorem from highly regarded book on
locally presentable categories (1994). Triggered further research elsewhere, including a paper by Hebert, Rosicky
(2001) salvaging classification theorem for uncountable cardinalities. Results from this output is currently being
used by the author to show that satisfiability for classical and inductive logic coincides for fragments of
first-order logic exceeding Horn logic, and to demonstrate the soundness of using classical logic to verify
cryptographic protocols using the closed world assumption inherent in the usual Dolev-Yao adversary models.
We present a locally finitely presentable category with a finitely presentable
regular generator G and a finitely presentable object A, such that A is not a coequalizer of morphisms whose
domains and codomains are finite coproducts of objects in G, thereby settling a problem by Gabriel and Ulmer.
We also show that in lambda-orthogonality classes the category of S-sorted tau-algebras for a lambda-ary
signature tau, lambda-presentable objects have a presentation by less than lambda generators and relations and
use this to exhibit an example of a reflective subcategory of a locally finitely presentable category which is
closed under directed colimits, but not a aleph_0-orthogonality class, disproving a characterization of
lambda-orthogonality classes in the book by Adamek and Rosicky. 1991 Math. Subj. Class.: Primary: 18C10;
secondary: 03C52,08A60, 08C05,18A40 Keywords: locally presentable category, presentable object, orthogonality
class, finitely presented, limit theory
[Show
Abstract]
@ARTICLE{opgu01,
author = {J.~{J}{\"u}{r}jens},
title = {On a problem of {Gabriel and Ulmer}},
journal = {Journal of Pure and Applied Algebra},
year = {2001},
volume = {158},
pages = {183--196},
abstract = {We present a locally finitely presentable category with a finitely
presentable regular generator G and a finitely presentable object
A, such that A is not a coequalizer of morphisms whose domains and
codomains are finite coproducts of objects in G, thereby settling
a problem by Gabriel and Ulmer. We also show that in lambda-orthogonality
classes the category of S-sorted tau-algebras for a lambda-ary signature
tau, lambda-presentable objects have a presentation by less than
lambda generators and relations and use this to exhibit an example
of a reflective subcategory of a locally finitely presentable category
which is closed under directed colimits, but not a aleph_0-orthogonality
class, disproving a characterization of lambda-orthogonality classes
in the book by Adamek and Rosicky. 1991 Math. Subj. Class.: Primary:
18C10; secondary: 03C52,08A60, 08C05,18A40 Keywords: locally presentable
category, presentable object, orthogonality class, finitely presented,
limit theory},
doi = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.2828},
file = {paper (pdf):http\://rgse.uni-koblenz.de/jj/publications/papers/gurevd.pdf:URL;paper
(ps):http\://rgse.uni-koblenz.de/jj/publications/papers/gurevd.ps:URL;paper
(gz):http\://rgse.uni-koblenz.de/jj/publications/papers/gurevd.ps.gz:URL},
keywords = {mathematicalLogic},
url = {\URL{http://www.jurjens.de/jan}}
}
[Show
BibTex] [ DOI ] [
paper (pdf) ] [
paper (ps) ] [ paper (gz) ]