|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 7900 occurrences of 4014 keywords
|
|
|
Results
Found 8451 publication records. Showing 8451 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
43 | James W. Gray III, John McLean |
Using temporal logic to specify and verify cryptographic protocols. |
CSFW |
1995 |
DBLP DOI BibTeX RDF |
specify, system penetrator, correctness requirements, verification, formal specification, formal methods, cryptography, protocols, formal verification, temporal logic, temporal logic, cryptographic protocols, verify |
43 | Markus Aderhold, Serge Autexier, Heiko Mantel (eds.) |
6th International Verification Workshop, VERIFY-2010, Edinburgh, UK, July 20-21, 2010 |
VERIFY@IJCAR |
2012 |
DBLP BibTeX RDF |
|
43 | Cliff B. Jones |
Abstractions Before Proofs. |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
43 | Emanuele Di Rosa, Enrico Giunchiglia, Massimo Narizzano, Gabriele Palma, Alessandra Puddu |
Automatic generation of high quality test sets via CBMC. |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
43 | Bernhard Beckert, Daniel Bruns, Sarah Grebing |
Mind the Gap: Formal Verification and the Common Criteria (Discussion Paper). |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
43 | Andrei Lapets |
User-friendly Support for Common Mathematical Concepts in a Lightweight Verifier. |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
43 | Shuling Wang, Xu Wang |
Proving Simpson's Four-Slot Algorithm Using Ownership Transfer. |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
43 | Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl |
Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays. |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
43 | Véronique Cortier |
Verification of Security Protocols. |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
43 | André Platzer |
Real Analysis for Complex Systems. |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
43 | Michael von Tessin |
Towards High-Assurance Multiprocessor Virtualisation. |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
43 | Joe Hurd |
Composable Packages for Higher Order Logic Theories. |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
43 | Mark Bickford |
Automated Proof of Authentication Protocols in a Logic of Events. |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
43 | Daniel Wasserrab, Denis Lohner |
Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing. |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
43 | Alessandro Carioni, Silvio Ghilardi, Silvio Ranise |
MCMT in the Land of Parametrized Timed Automata. |
VERIFY@IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
34 | Zhengyou Zhang, Olivier D. Faugeras |
Estimation of Displacements from Two 3-D Frames Obtained From Stereo. |
IEEE Trans. Pattern Anal. Mach. Intell. |
1992 |
DBLP DOI BibTeX RDF |
3D displacement estimation, line segment matching, hypothesize-and-verify paradigm, complexity, image segmentation, motion estimation, Kalman filters, stereo, stereo image processing, extended Kalman filter, rigidity constraints |
31 | Craig M. Wittenbrink, Alex Pang, Suresh K. Lodha |
Glyphs for Visualizing Uncertainty in Vector Fields. |
IEEE Trans. Vis. Comput. Graph. |
1996 |
DBLP DOI BibTeX RDF |
Verify visualization, wind profilers, doppler radar, wind barbs, icons |
31 | Francesca Cesarini, Marco Gori, Simone Marinai, Giovanni Soda |
A system for data extraction from forms of known class. |
ICDAR |
1995 |
DBLP DOI BibTeX RDF |
information fields, hypothesize-and-verify paradigm, autoassociator-based connectionist model, instruction fields, noisy forms, pattern recognition, data extraction, forms processing, attributed relational graphs |
29 | Jingmin Zhou, Adam J. Carlson, Matt Bishop |
Verify Results of Network Intrusion Alerts Using Lightweight Protocol Analysis. |
ACSAC |
2005 |
DBLP DOI BibTeX RDF |
|
27 | Wentao Qu, Minglu Li 0001, Chuliang Weng |
An Active Trusted Model for Virtual Machine Systems. |
ISPA |
2009 |
DBLP DOI BibTeX RDF |
trusted virtual machine, measure, verify, active model |
27 | Franco Fummi, A. Marshall, Laura Pozzi, Mariagiovanna Sami |
Minimizing the Application Time for Manufacturer Testing of FPGA (Abstract). |
FPGA |
1998 |
DBLP DOI BibTeX RDF |
VERIFY |
27 | Bernhard Beckert, Gerwin Klein |
Title, Preface, Table of Contents. |
VERIFY |
2008 |
DBLP BibTeX RDF |
|
27 | Niusha Hakimipour, Paul A. Strooper, Roger Duke |
Exploring Model-Based Development for the Verification of Real-Time Java Code. |
VERIFY |
2008 |
DBLP BibTeX RDF |
|
27 | Hasan Amjad, Richard Bornat |
Model Checking for Stability Analysis in Rely-Guarantee Proofs. |
VERIFY |
2008 |
DBLP BibTeX RDF |
|
27 | Bernhard Beckert, Gerwin Klein (eds.) |
Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, Sydney, Australia, August 10-11, 2008 |
VERIFY |
2008 |
DBLP BibTeX RDF |
|
27 | Matthias Daum 0001, Jan Dörrenbächer, Sebastian Bogan |
Model Stack for the Pervasive Verification of a Microkernel-based Operating System. |
VERIFY |
2008 |
DBLP BibTeX RDF |
|
27 | David A. Cock |
Bitfields and Tagged Unions in C: Verification through Automatic Generation. |
VERIFY |
2008 |
DBLP BibTeX RDF |
|
27 | Gurvan Le Guernic |
Precise Dynamic Verification of Confidentiality. |
VERIFY |
2008 |
DBLP BibTeX RDF |
|
27 | Simon Bäumler, Florian Nafz, Michael Balser, Wolfgang Reif |
Compositional Proofs with Symbolic Execution. |
VERIFY |
2008 |
DBLP BibTeX RDF |
|
27 | Richard Bubel, Reiner Hähnle, Peter H. Schmitt |
Specification Predicates with Explicit Dependency Information. |
VERIFY |
2008 |
DBLP BibTeX RDF |
|
27 | Gernot Heiser |
Operating System Verification for Real Use. |
VERIFY |
2008 |
DBLP BibTeX RDF |
|
27 | Gilles Barthe |
Certificate Translation. |
VERIFY |
2008 |
DBLP BibTeX RDF |
|
27 | Till Mossakowski, Christian Maeder, Klaus Lüttich |
The Heterogeneous Tool Set (Hets). |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | André Platzer |
Combining Deduction and Algebraic Constraints for Hybrid System Analysis. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Tobias Nipkow |
Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Borislav Gajanovic, Bernhard Rumpe |
ALICE: An Advanced Logic for Interactive Component Engineering. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Aaron Stump |
Lightweight Verification with Dependent Types. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Jia Meng, Lawrence C. Paulson, Gerwin Klein |
A Termination Checker for Isabelle Hoare Logic. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Philipp Rümmer |
A Sequent Calculus for Integer Arithmetic with Counterexample Generation. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Mamoun Filali |
A Mechanization of Phylogenetic Trees. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Bernhard Beckert (eds.) |
Proceedings of 4th International Verification Workshop in connection with CADE-21, Bremen, Germany, July 15-16, 2007 |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Eyad Alkassar, Mark A. Hillebrand, Steffen Knapp, Rostislav Rusev, Sergey Tverdyshev |
Formal Device and Programming Model for a Serial Interface. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Bruno Langenstein, Andreas Nonnengart, Georg Rock, Werner Stephan 0001 |
A History-based Verification of Distributed Applications. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Pascal Fontaine |
Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Peter H. Schmitt, Benjamin Weiß 0001 |
Inferring Invariants by Symbolic Execution. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Wojciech Mostowski |
Fully Verified Java Card API Reference Implementation. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Olivera Pavlovic, Ralf Pinger, Maik Kollmann |
Automation of Formal Verification of PLC Programs Written in IL. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Daniel Larsson, Reiner Hähnle |
Symbolic Fault Injection. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
27 | Cesare Tinelli |
Trends and Challenges in Satisfiability Modulo Theories. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
26 | Osman Hasan, Sofiène Tahar |
Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. |
J. Autom. Reason. |
2008 |
DBLP DOI BibTeX RDF |
Coupon collector’s problem, Probabilistic analysis, Higher-order-logic, Probability theory, Statistical properties, HOL theorem prover |
26 | Zhicheng Wen, Huaikou Miao, Hongwei Zeng |
Generating Proof Obligation to Verify Object-Z Specification. |
ICSEA |
2006 |
DBLP DOI BibTeX RDF |
formal specification, Object-Z, proof obligation |
26 | Christian Skalka, Xiaoyang Sean Wang |
Trust but verify: authorization for web services. |
SWS |
2004 |
DBLP DOI BibTeX RDF |
access control logic, web services, distributed authorization |
22 | Alexandre Janot, Pierre-Olivier Vandanjon, Maxime Gautier |
Using robust regressions and residual analysis to verify the reliability of LS estimation: Application in robotics. |
IROS |
2009 |
DBLP DOI BibTeX RDF |
|
22 | Xinyu Feng 0001, Zhong Shao, Yu Guo, Yuan Dong |
Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
22 | C. Richard Ho, Michael Theobald, Martin M. Deneroff, Ron O. Dror, Joseph Gagliardo, David E. Shaw |
Early formal verification of conditional coverage points to identify intrinsically hard-to-verify logic. |
DAC |
2008 |
DBLP DOI BibTeX RDF |
conditional coverage, inconclusive results, formal verification, code coverage, verifiability, coverage hole |
22 | Domenico Bianculli, Carlo Ghezzi, Paola Spoletini |
A Model Checking Approach to Verify BPEL4WS Workflows. |
SOCA |
2007 |
DBLP DOI BibTeX RDF |
|
22 | Erik Reeber, Jun Sawada |
Combining ACL2 and an automated verification tool to verify a multiplier. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
model checking, theorem proving, hardware verification |
22 | Jia Xu |
Making Software Timing Properties Easier to Inspect and Verify. |
IEEE Softw. |
2003 |
DBLP DOI BibTeX RDF |
preruntime scheduling, verification, real time, predictability, software, code, inspection, undecidability, timing properties, state space explosion |
22 | Miroslav N. Velev |
Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer. |
DATE |
2002 |
DBLP DOI BibTeX RDF |
|
22 | Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl |
Abstracting WS1S Systems to Verify Parameterized Networks. |
TACAS |
2000 |
DBLP DOI BibTeX RDF |
|
22 | A. N. Trahtman |
An Algorithm to Verify Local Threshold Testability of Deterministic Finite Automata. |
WIA |
1999 |
DBLP DOI BibTeX RDF |
locally threshold testable, semigroup AMS subject classification 68Q25, 68Q68, 20M07, algorithm, deterministic finite automaton, 68Q45 |
21 | Vahab S. Mirrokni, Alexander Skopalik |
On the complexity of nash dynamics and sink equilibria. |
EC |
2009 |
DBLP DOI BibTeX RDF |
potential games, sink equilibria, nash equilibria |
19 | Olivier Coudert |
An efficient algorithm to verify generalized false paths. |
DAC |
2010 |
DBLP DOI BibTeX RDF |
co-sensitization, generalized false path, timing exception, formal verification, correctness, SAT, sensitization, false path, SDC |
19 | Lei Liu 0039, Sen Zhang, Lu Hong Diao, Shu Ying Yan, Cungen Cao 0001 |
Using Concept Space to Verify Hyponymy in Building a Hyponymy Lexicon. |
AICI |
2009 |
DBLP DOI BibTeX RDF |
hyponymy, relation acquisition, hyponymy verification, knowledge acquisition |
19 | Colin O'Halloran |
Guess and Verify - Back to the Future. |
FM |
2009 |
DBLP DOI BibTeX RDF |
Models, Verification, Software, Automation, Cost, Proof, Simulink |
19 | German Florez-Larrahondo, Walker Haddock |
Aspect oriented programming with hidden markov models to verify design use cases. |
AOSD |
2009 |
DBLP DOI BibTeX RDF |
aspect-oriented programming, stochastic models, runtime verification, acm proceedings |
19 | Jonathan Ezekiel, Alessio Lomuscio |
Combining fault injection and model checking to verify fault tolerance in multi-agent systems. |
AAMAS (1) |
2009 |
DBLP BibTeX RDF |
fault tolerance, model checking, fault injection, epistemic logic |
19 | Bruno Mermet, Gaële Simon |
GDT4MAS: an extension of the GDT model to specify and to verify MultiAgent systems. |
AAMAS (1) |
2009 |
DBLP BibTeX RDF |
GDTs, verification, specification, temporal logic, multiagent systems |
19 | Javier Cubo, Michele Sama, Franco Raimondi, David S. Rosenblum |
A Model to Design and Verify Context-Aware Adaptive Service Composition. |
IEEE SCC |
2009 |
DBLP DOI BibTeX RDF |
|
19 | Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, Lori A. Clarke |
Combining symbolic execution with model checking to verify parallel numerical programs. |
ACM Trans. Softw. Eng. Methodol. |
2008 |
DBLP DOI BibTeX RDF |
model checking, parallel programming, concurrency, MPI, Message Passing Interface, high performance computing, symbolic execution, floating-point, Spin, Finite-state verification, numerical program |
19 | Stephen F. Siegel, Louis F. Rossi |
Analyzing BlobFlow: A Case Study Using Model Checking to Verify Parallel Scientific Software. |
PVM/MPI |
2008 |
DBLP DOI BibTeX RDF |
|
19 | Wencai Guo, Chuang Lin 0002 |
A Formal Approach to Verify Grid Service Composition Based on Interaction Pattern. |
APSCC |
2008 |
DBLP DOI BibTeX RDF |
|
19 | Andreas Binzenhöfer, Daniel Schlosser, Kurt Tutschku, Markus Fiedler |
An Autonomic Approach to Verify End-to-End Communication Quality. |
Integrated Network Management |
2007 |
DBLP DOI BibTeX RDF |
|
19 | Haiyang Sun, Jian Yang 0001 |
Exploiting CoBTx-Net to Verify the Reliability of Collaborative Business Transactions. |
APSCC |
2007 |
DBLP DOI BibTeX RDF |
|
19 | K. Rustan M. Leino, Wolfram Schulte |
Using History Invariants to Verify Observers. |
ESOP |
2007 |
DBLP DOI BibTeX RDF |
|
19 | Sujatha Kuppuraju, Aravind Kumar, Geetha Presenna Kumari |
Case Study to Verify the Interoperability of a Service Oriented Architecture Stack. |
IEEE SCC |
2007 |
DBLP DOI BibTeX RDF |
|
19 | Pavel Krcál, Wang Yi 0001 |
Communicating Timed Automata: The More Synchronous, the More Difficult to Verify. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
19 | Michael J. May, Carl A. Gunter, Insup Lee 0001 |
Privacy APIs: Access Control Techniques to Analyze and Verify Legal Privacy Policies. |
CSFW |
2006 |
DBLP DOI BibTeX RDF |
|
19 | Timothy Fraser, Nick L. Petroni Jr., William A. Arbaugh |
Applying flow-sensitive CQUAL to verify MINIX authorization check placement. |
PLAS |
2006 |
DBLP DOI BibTeX RDF |
CQUAL, static analysis, type qualifiers, MINIX |
19 | Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, Lori A. Clarke |
Using model checking with symbolic execution to verify parallel numerical programs. |
ISSTA |
2006 |
DBLP DOI BibTeX RDF |
model checking, parallel programming, concurrency, MPI, message passing interface, high performance computing, symbolic execution, floating-point, spin, finite state verification, numerical program |
19 | Denis Meron, Bruno Mermet |
A Tool Architecture to Verify Properties of Multiagent System at Runtime. |
PROMAS |
2006 |
DBLP DOI BibTeX RDF |
|
19 | Ahsan Habib 0001, Dongyan Xu, Mikhail J. Atallah, Bharat K. Bhargava, John Chuang |
A Tree-Based Forward Digest Protocol to Verify Data Integrity in Distributed Media Streaming. |
IEEE Trans. Knowl. Data Eng. |
2005 |
DBLP DOI BibTeX RDF |
message digest and media streaming, Data integrity |
19 | Mitsuhiro T. Nakao, Kouji Hashimoto, Yoshitaka Watanabe |
A Numerical Method to Verify the Invertibility of Linear Elliptic Operators with Applications to Nonlinear Problems. |
Computing |
2005 |
DBLP DOI BibTeX RDF |
Numerical verification, unique solvability of linear elliptic problem, finite element method |
19 | Egon Börger |
Linking the Meaning of Programs to What the Compiler Can Verify. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
19 | Jens Brandt 0001, Klaus Schneider 0001 |
Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry. |
ICFEM |
2005 |
DBLP DOI BibTeX RDF |
|
19 | Kees M. van Hee, Olivia Oanea, Natalia Sidorova |
Colored Petri Nets to Verify Extended Event-Driven Process Chains. |
OTM Conferences (1) |
2005 |
DBLP DOI BibTeX RDF |
Extended EPCs, verification, semantics, colored Petri nets |
19 | Carole Durocher, Franck Multon, Richard Kulpa |
Dynamic Control of Captured Motions to Verify New Constraints. |
Gesture Workshop |
2005 |
DBLP DOI BibTeX RDF |
take-off, optimization, constraints, dynamic control |
19 | Dan E. Willard |
On the Partial Respects in Which a Real Valued Arithmetic System Can Verify Its Tableaux Consistency. |
TABLEAUX |
2005 |
DBLP DOI BibTeX RDF |
|
19 | Nik Swoboda, Gerard Allwein |
Using DAG transformations to verify Euler/Venn homogeneous and Euler/Venn FOL heterogeneous rules of inference. |
Softw. Syst. Model. |
2004 |
DBLP DOI BibTeX RDF |
Euler and Venn diagrams, Graph transformation, Diagrammatic reasoning, Proof verification |
19 | Aydan R. Yumerefendi, Jeffrey S. Chase |
Trust but verify: accountability for network services. |
ACM SIGOPS European Workshop |
2004 |
DBLP DOI BibTeX RDF |
|
19 | Abhay Vardhan, Koushik Sen, Mahesh Viswanathan 0001, Gul Agha |
Actively Learning to Verify Safety for FIFO Automata. |
FSTTCS |
2004 |
DBLP DOI BibTeX RDF |
|
19 | Sin Yeung Lee, Tok Wang Ling |
Verify Updating Trigger Correctness. |
DEXA |
1999 |
DBLP DOI BibTeX RDF |
|
19 | Cindy Eisner |
Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
19 | Dieter Fensel, Arno Schönegge |
Using KIV to Specify and Verify Architectures of Knowledge-Based Systems. |
ASE |
1997 |
DBLP DOI BibTeX RDF |
reusable elements, Karlsruhe interactive verifier, algorithmic specification, interactive theorem prover, proof management, proof reuse, formal specification, formal specifications, knowledge-based systems, specification language, abstract data types, dynamic logic, functional specification |
19 | Homer H. Chen, Thomas S. Huang |
Using Motion from Orthographic Views to Verify 3-D Point Matches. |
IEEE Trans. Pattern Anal. Mach. Intell. |
1991 |
DBLP DOI BibTeX RDF |
3D point matching, depth error effect, orthographic views, pattern recognition, pattern recognition, motion estimate, picture processing, picture processing, image matching, motion analysis |
19 | Richard Lai 0001, Ken R. Parker, Tharam S. Dillon |
On Using Protean To Verify ISO FTAM Protocol. |
CAV |
1990 |
DBLP DOI BibTeX RDF |
|
17 | N. R. Sunitha, B. B. Amberker |
A new method of verifying digital signatures in e-cheque processing. |
ICON |
2008 |
DBLP DOI BibTeX RDF |
|
17 | Francine Bacchini, Gabe Moretti, Harry Foster, Janick Bergeron, Masayuki Nakamura, Shrenik Mehta, Laurent Ducousso |
Is methodology the highway out of verification hell? |
DAC |
2005 |
DBLP DOI BibTeX RDF |
verification, formal verification, methodology, assertions |
16 | Junjie An, Zhidao Zhou, Linfang Wang, Wang Ye, Weizeng Li, Hanghang Gao, Zhi Li, Jinghui Tian, Yan Wang, Hongyang Hu, Jinshan Yue, Lingyan Fan, Shibing Long, Qi Liu 0010, Chunmeng Dou |
Write-Verify-Free MLC RRAM Using Nonbinary Encoding for AI Weight Storage at the Edge. |
IEEE Trans. Very Large Scale Integr. Syst. |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Shurui Bai, Donn Emmanuel Gonda, Khe Foon Hew |
Write-Curate-Verify: A Case Study of Leveraging Generative AI for Scenario Writing in Scenario-Based Learning. |
IEEE Trans. Learn. Technol. |
2024 |
DBLP DOI BibTeX RDF |
|
Displaying result #1 - #100 of 8451 (100 per page; Change: ) Pages: [ 1][ 2][ 3][ 4][ 5][ 6][ 7][ 8][ 9][ 10][ >>] |
|