Verification of an off-line checker tor priority queues

被引：0
|
作者：
de Nivelle, H [1 ]
Piskac, R [1 ]
机构：
[1] Max Planck Inst Informat, D-66123 Saarbrucken, Germany
来源：
SEFM 2005: Third IEEE International Conference on Software Engineering and Formal Methods, Proceedings | 2005年
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We formally verify the result checker for priority queues that is implemented in LEDA. We have developed a method, based on the notion of implementation, which links abstract specifications to concrete implementations. The method allows non-determinism in the abstract specifications that the concrete implementations have to fill in. We have formally verified that, if the checker has not reported an error up to a certain moment, then the structure it checks has behaved like a priority queue up to that moment. For the verification, we have used the first-order theorem prover Saturate.
引用
收藏
页码：210 / 219
页数：10
相关论文
共 50 条
  • [41] Off-line Signature Verification Using Linear Regression Classifier
    Xu, Bo
    Lin, Daozhi
    Chao, Hongyang
    Li, Weifeng
    Liao, Qingmin
    PROCEEDINGS OF THE 4TH INTERNATIONAL CONFERENCE ON INFORMATION TECHNOLOGY AND MANAGEMENT INNOVATION, 2015, 28 : 1144 - 1148
  • [42] Off-line signature verification with PSO-NN algorithm
    Das, A. Taylan
    Dulger, L. Canan
    2007 22ND INTERNATIONAL SYMPOSIUM ON COMPUTER AND INFORMATION SCIENCES, 2007, : 92 - 97
  • [43] A peripheral feature based approach for off-line signature verification
    Fang, B
    Leung, CH
    Tang, YY
    Kwok, PCK
    Tse, KW
    Wong, YK
    PROCEEDINGS OF THE FIFTH JOINT CONFERENCE ON INFORMATION SCIENCES, VOLS 1 AND 2, 2000, : A236 - A239
  • [44] A human-centric off-line signature verification system
    Coetzer, Hanno
    Sabourin, Robert
    ICDAR 2007: NINTH INTERNATIONAL CONFERENCE ON DOCUMENT ANALYSIS AND RECOGNITION, VOLS I AND II, PROCEEDINGS, 2007, : 153 - +
  • [45] Off-line signature verification using structural feature correspondence
    Huang, K
    Yan, H
    PATTERN RECOGNITION, 2002, 35 (11) : 2467 - 2477
  • [46] Generation of Duplicated Off-Line Signature Images for Verification Systems
    Diaz, Moises
    Ferrer, Miguel A.
    Eskander, George S.
    Sabourin, Robert
    IEEE TRANSACTIONS ON PATTERN ANALYSIS AND MACHINE INTELLIGENCE, 2017, 39 (05) : 951 - 964
  • [47] Off-line signature verification using generated training samples
    Fang, B
    Leung, CH
    Tang, YY
    OPTICAL INFORMATION PROCESSING TECHNOLOGY, 2002, 4929 : 388 - 397
  • [48] OFF-LINE WRITER VERIFICATION USING ORDINARY CHARACTERS AS THE OBJECT
    YOSHIMURA, I
    YOSHIMURA, M
    PATTERN RECOGNITION, 1991, 24 (09) : 909 - 915
  • [49] Learning strategies and classification methods for off-line signature verification
    Srihari, SN
    Xu, AH
    Kalera, MK
    NINTH INTERNATIONAL WORKSHOP ON FRONTIERS IN HANDWRITING RECOGNITION, PROCEEDINGS, 2004, : 161 - 166
  • [50] Translating off-line schedules into task attributes for fixed priority scheduling
    Dobrin, R
    Fohler, G
    Puschner, P
    22ND IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2001, : 225 - 234
12345